From 19783cea9664e5ac0b14419b4aa961716010aafb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jan 2022 21:32:06 +0100
Subject: Introduce "AIgnore" for the avalues

---
 src/Invariants.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'src/Invariants.ml')

diff --git a/src/Invariants.ml b/src/Invariants.ml
index 3fc390b5..23f7d456 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -593,14 +593,13 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 assert (child.V.ty = borrowed_aty)
             | V.AIgnoredSharedLoan child_av ->
                 assert (child_av.V.ty = aloan_get_expected_child_type aty))
-        | V.ASymbolic aproj, ty ->
+        | V.ASymbolic aproj, ty -> (
             let ty1 = Subst.erase_regions ty in
-            let ty2 =
-              match aproj with
-              | V.AProjLoans sv | V.AProjBorrows (sv, _) ->
-                  Subst.erase_regions sv.V.sv_ty
-            in
-            assert (ty1 = ty2)
+            match aproj with
+            | V.AProjLoans sv | V.AProjBorrows (sv, _) ->
+                let ty2 = Subst.erase_regions sv.V.sv_ty in
+                assert (ty1 = ty2)
+            | V.AEndedProjLoans | V.AEndedProjBorrows -> ())
         | _ -> failwith "Erroneous typing");
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
-- 
cgit v1.2.3