summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-04 23:11:14 +0100
committerSon Ho2022-01-04 23:11:14 +0100
commit1e83bc8b14c97170833a5af721e58ff746d61317 (patch)
tree63150120c3a66e3f0c80ffd32e21a7f0f9a95860
parentab2637af8b82f13be8ac38a800368bce6bbd10e5 (diff)
Cleanup a bit
-rw-r--r--src/Invariants.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 9390436c..fec6b2ed 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -9,7 +9,6 @@ module Subst = Substitute
module A = CfimAst
module L = Logging
open InterpreterUtils
-open Errors
let debug_invariants : bool ref = ref false
@@ -404,7 +403,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Abstract (V.ASharedLoan (_, sv, _)) ->
assert (sv.V.ty = ref_ty)
| _ -> failwith "Inconsistent context")
- | V.MutBorrow (bid, bv), T.Mut ->
+ | V.MutBorrow (_, bv), T.Mut ->
assert (
(* Check that the borrowed value has the proper type *)
bv.V.ty = ref_ty)
@@ -478,7 +477,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| V.ABottom, _ -> (* Nothing to check *) ()
| V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
match (bc, rkind) with
- | V.AMutBorrow (bid, av), T.Mut ->
+ | V.AMutBorrow (_, av), T.Mut ->
(* Check that the child value has the proper type *)
assert (av.V.ty = ref_ty)
| V.ASharedBorrow bid, T.Shared -> (