From df6b9158ede367ce175816fbf37485a6cd71431f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 9 Jun 2023 10:14:51 +0200
Subject: [PATCH] avoid fractional_half_2
---
theories/logic/spec_ra.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 69cabd2..cba58c5 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -203,8 +203,7 @@ Section mapsto.
Proof.
iIntros "Hl1 Hl2".
iDestruct (mapstoS_agree with "Hl1 Hl2") as %?. simplify_eq.
- iSplit; eauto.
- iApply (fractional_half_2 with "Hl1 Hl2").
+ iSplit; eauto. iCombine "Hl1 Hl2" as "?". done.
Qed.
End mapsto.
--
GitLab