summaryrefslogtreecommitdiff
path: root/src/InterpreterBorrows.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-06 11:01:44 +0100
committerSon Ho2022-01-06 11:01:44 +0100
commit6a3faa82e09e3fbf23014b53a2b40d420bc70c9b (patch)
tree97cb2ba076c8229a76d168b5ec2ce8e6a87b906f /src/InterpreterBorrows.ml
parent8cac3c5cb5f9c36ffa878cf32ce858d171e4e3c8 (diff)
Cleanup a bit more the dependencies and activate more warnings/errors
Diffstat (limited to '')
-rw-r--r--src/InterpreterBorrows.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 33501939..b60f0973 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1,12 +1,8 @@
module T = Types
module V = Values
-module E = Expressions
module C = Contexts
module Subst = Substitute
-module A = CfimAst
module L = Logging
-module Inv = Invariants
-module S = Synthesis
open Utils
open InterpreterUtils
open InterpreterProjectors