From 1af9e5d66336e2892cbb2b12fb446eb740e10f17 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 14 May 2023 15:27:44 +0200
Subject: [PATCH] add iCombine FIXME
---
iris/base_logic/lib/ghost_var.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 6139e4088..b41c31efc 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -82,6 +82,7 @@ Section lemmas.
(* higher cost than the Fractional instance, which is used for a1 = a2 *)
Proof.
rewrite /CombineSepAs /IsOp => ->. iIntros "[H1 H2]".
+ (* FIXME: in the future a single [iCombine] should suffice here. *)
iCombine "H1 H2" gives %[_ ->].
by iCombine "H1 H2" as "H".
Qed.
--
GitLab