From 4417beb8bfa43f89c09a027e8dd55550bf8f7a63 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 30 Nov 2016 09:37:25 +0100
Subject: [PATCH] Partly revert a9880321b3 and 9ae19ed597.
Also, higher cost for [elim_modal_bupd_fupd], so that it is not taken in place of [elim_modal_fupd_fupd] in spec patterns.
---
base_logic/lib/fancy_updates.v | 12 ++----------
1 file changed, 2 insertions(+), 10 deletions(-)
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index 364de0720..f85051320 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -176,12 +176,12 @@ Section proofmode_classes.
Proof. rewrite /IntoModal. apply fupd_intro. Qed.
Global Instance elim_modal_bupd_fupd E1 E2 P Q :
- ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+ ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed.
Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
- ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 10.
+ ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes.
@@ -221,12 +221,4 @@ Proof.
iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
Qed.
-
-Global Instance elim_modal_step_fupd E1 E2 E3 E4 P Q :
- ElimModal (|={E1,E2}=>â–·|={E2,E3}=> P) P
- (|={E1,E2}=>â–·|={E2,E4}=> Q) (|={E3,E4}=> Q).
-Proof.
- iIntros "[A B]". iMod "A". iModIntro. iNext. iMod "A". by iApply "B".
-Qed.
-
End step_fupd.
--
GitLab