diff options
| author | Son Ho | 2022-01-28 01:52:58 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-28 01:52:58 +0100 |
| commit | dc9d2c64bc2948bfdff78f1d2abae45ec9b4972c (patch) | |
| tree | c7dba718348778a47003c1a99717ed61f97ff5e3 /src/InterpreterBorrows.ml | |
| parent | 3af881c9a5c8935e2238509d3447ec42e29b8404 (diff) | |
Make a lot of small modifications
Diffstat (limited to '')
| -rw-r--r-- | src/InterpreterBorrows.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index e7031d4c..f430c15d 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -11,6 +11,9 @@ open InterpreterUtils open InterpreterBorrowsCore open InterpreterProjectors +(** The local logger *) +let log = InterpreterBorrowsCore.log + (** Auxiliary function to end borrows: lookup a borrow in the environment, update it (by returning an updated environment where the borrow has been replaced by [Bottom])) if we can end the borrow (for instance, it is not |