summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Invariants.ml6
-rw-r--r--src/Modules.ml4
2 files changed, 1 insertions, 9 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 08ae6b4a..b67fa3a2 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -3,15 +3,11 @@
module T = Types
module V = Values
-open Scalars
module E = Expressions
-open Errors
module C = Contexts
module Subst = Substitute
module A = CfimAst
module L = Logging
-open TypesUtils
-open ValuesUtils
open InterpreterUtils
let debug_invariants : bool ref = ref false
@@ -337,7 +333,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
let info = { outer_borrow = false; outer_shared = false } in
visitor#visit_eval_ctx info ctx
-let check_typing_invariant (ctx : C.eval_ctx) : unit = ()
+let check_typing_invariant (_ctx : C.eval_ctx) : unit = ()
let check_invariants (ctx : C.eval_ctx) : unit =
check_loans_borrows_relation_invariant ctx;
diff --git a/src/Modules.ml b/src/Modules.ml
index 3be1c742..5b76880f 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -1,9 +1,5 @@
open Yojson.Basic
-open Identifiers
open Types
-open OfJsonBasic
-open Scalars
-open Values
open CfimAst
(** Module declaration *)