From 2e1808c5abf2c5dbdd5f8345a03197169ad656e7 Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Wed, 5 Feb 2025 08:14:15 +0100
Subject: [PATCH] fix divergence without vProp annotation

---
 theories/typing/type.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index e40f037b..1245b1d6 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -476,7 +476,7 @@ Section type.
   Qed.
 
   Lemma shr_locsE_split_tok l n m tid :
-    na_own tid (shr_locsE l (n + m)) ⊣⊢
+    na_own tid (shr_locsE l (n + m)) ⊣⊢@{vPropI _}
       na_own tid (shr_locsE l n) ∗ na_own tid (shr_locsE (l +ₗ n) m).
   Proof.
     rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
-- 
GitLab