diff options
Diffstat (limited to 'compiler/InterpreterBorrows.mli')
| -rw-r--r-- | compiler/InterpreterBorrows.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/InterpreterBorrows.mli b/compiler/InterpreterBorrows.mli index a2a1cfde..9e407399 100644 --- a/compiler/InterpreterBorrows.mli +++ b/compiler/InterpreterBorrows.mli @@ -197,7 +197,7 @@ type merge_duplicates_funcs = { *) } -(** Merge two abstractions together. +(** Merge an abstraction into another abstraction. We insert the result of the merge in place of the first abstraction (this helps preserving the structure of the environment, when computing loop |