summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterBorrows.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index b60f0973..38c79b66 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -5,6 +5,7 @@ module Subst = Substitute
module L = Logging
open Utils
open InterpreterUtils
+open InterpreterBorrowsCore
open InterpreterProjectors
(** Auxiliary function to end borrows: lookup a borrow in the environment,