summaryrefslogtreecommitdiff
path: root/src/InterpreterProjectors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/InterpreterProjectors.ml')
-rw-r--r--src/InterpreterProjectors.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index c3fd0708..92ea6483 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -8,6 +8,7 @@ open TypesUtils
open ValuesUtils
open Utils
open InterpreterUtils
+open InterpreterBorrowsCore
(** Auxiliary function.