summaryrefslogtreecommitdiff
path: root/src/Invariants.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Invariants.ml')
-rw-r--r--src/Invariants.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 11b00381..86fa3d46 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -433,8 +433,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Abstract (V.AMutBorrow (_, sv)) ->
assert (Subst.erase_regions sv.V.ty = ty)
| _ -> failwith "Inconsistent context"))
- | V.Symbolic spc, ty ->
- let ty' = Subst.erase_regions spc.V.svalue.V.sv_ty in
+ | V.Symbolic sv, ty ->
+ let ty' = Subst.erase_regions sv.V.sv_ty in
assert (ty' = ty)
| _ -> failwith "Erroneous typing");
(* Continue exploring to inspect the subterms *)