summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/InterpreterBorrows.ml')
-rw-r--r--src/InterpreterBorrows.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 38c79b66..ca1f87f1 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -4,6 +4,7 @@ module C = Contexts
module Subst = Substitute
module L = Logging
open Utils
+open ValuesUtils
open InterpreterUtils
open InterpreterBorrowsCore
open InterpreterProjectors