From 7cfa93e88408b77aa316168347f263d80578723f Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 5 Mar 2018 10:57:15 +0100
Subject: [PATCH] Use MakeMonPredAd in ElimModal instances.
---
theories/proofmode/monpred.v | 14 ++++++++------
1 file changed, 8 insertions(+), 6 deletions(-)
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 228e1d454..ba13064ec 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -363,10 +363,11 @@ Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q Q' i :
ElimModal φ ð“Ÿ ð“Ÿ' (|==> Q i) (|==> Q' i) →
ElimModal φ ð“Ÿ ð“Ÿ' ((|==> Q) i) ((|==> Q') i).
Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
-Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ P ð“Ÿ' ð“ ð“ ' i:
- ElimModal φ (|==> P i) ð“Ÿ' ð“ ð“ ' →
+Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ P ð“Ÿ ð“Ÿ' ð“ ð“ ' i:
+ MakeMonPredAt i P 𓟠→
+ ElimModal φ (|==> ð“Ÿ) ð“Ÿ' ð“ ð“ ' →
ElimModal φ ((|==> P) i) ð“Ÿ' ð“ ð“ '.
-Proof. by rewrite /ElimModal monPred_at_bupd. Qed.
+Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} φ ð“Ÿ ð“Ÿ' Q i :
AddModal ð“Ÿ ð“Ÿ' (|==> Q i)%I → AddModal ð“Ÿ ð“Ÿ' ((|==> Q) i).
@@ -468,10 +469,11 @@ Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 ð“Ÿ ð“Ÿ' Q
ElimModal φ ð“Ÿ ð“Ÿ' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
ElimModal φ ð“Ÿ ð“Ÿ' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
Proof. by rewrite /ElimModal !monPred_at_fupd. Qed.
-Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ E1 E2 P ð“Ÿ' ð“ ð“ ' i :
- ElimModal φ (|={E1,E2}=> P i) ð“Ÿ' ð“ ð“ ' →
+Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ E1 E2 P ð“Ÿ ð“Ÿ' ð“ ð“ ' i :
+ MakeMonPredAt i P 𓟠→
+ ElimModal φ (|={E1,E2}=> ð“Ÿ) ð“Ÿ' ð“ ð“ ' →
ElimModal φ ((|={E1,E2}=> P) i) ð“Ÿ' ð“ ð“ '.
-Proof. by rewrite /ElimModal monPred_at_fupd. Qed.
+Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 ð“Ÿ ð“Ÿ' Q i :
AddModal ð“Ÿ ð“Ÿ' (|={E1,E2}=> Q i) → AddModal ð“Ÿ ð“Ÿ' ((|={E1,E2}=> Q) i).
--
GitLab