From a9880321b3e2fc16ec1f676d5e675154dabf8ae2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 30 Nov 2016 09:14:16 +0100
Subject: [PATCH] Higher cost for [elim_modal_fupd_fupd to give priority on
[elim_modal_step_fupd.
---
base_logic/lib/fancy_updates.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index 9a4bb21b9..364de0720 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -179,9 +179,9 @@ Section proofmode_classes.
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
- Qed.
+ Qed.
Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
- ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+ ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 10.
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes.
--
GitLab