From fd42adfe6236b6bebacb963e8fed3f7d1f935e26 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 30 Nov 2016 11:04:06 +0100
Subject: [PATCH] Comment.
---
base_logic/lib/fancy_updates.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index f85051320..f9540df97 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -175,6 +175,9 @@ Section proofmode_classes.
Global Instance into_modal_fupd E P : IntoModal P (|={E}=> P).
Proof. rewrite /IntoModal. apply fupd_intro. Qed.
+ (* Put a lower priority compared to [elim_modal_fupd_fupd], so that
+ it is not taken when the first parameter is not specified (in
+ spec. patterns). *)
Global Instance elim_modal_bupd_fupd E1 E2 P Q :
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
Proof.
--
GitLab