From d870e5cfc2ca490d421f78ffb9d93ee73a9f58e5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Feb 2018 19:54:32 +0100
Subject: [PATCH] monpred: note that notation is somewhat broken
---
theories/bi/monpred.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index ec18ef8dd..0ce6daec6 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -816,6 +816,7 @@ Implicit Types P Q : monPred.
Global Instance monPred_bupd_facts `{BUpdFacts PROP} : BUpdFacts monPredSI.
Proof.
split; unseal; unfold monPred_bupd_def, monPred_upclosed.
+ (* Note: Notation is somewhat broken here. *)
- intros n P Q HPQ. split=>/= i. by repeat f_equiv.
- intros P. split=>/= i. apply bi.forall_intro=>?. rewrite bi.pure_impl_forall.
apply bi.forall_intro=><-. apply bupd_intro.
@@ -868,6 +869,7 @@ Proof. split; try apply _; by unseal. Qed.
Global Instance monPred_fupd_facts `{FUpdFacts PROP} : FUpdFacts monPredSI.
Proof.
split; first apply _; unseal; unfold monPred_fupd_def, monPred_upclosed.
+ (* Note: Notation is somewhat broken here. *)
- intros E1 E2 n P Q HPQ. split=>/= i. by repeat f_equiv.
- intros E1 E2 P HE12. split=>/= i.
do 2 setoid_rewrite bi.pure_impl_forall. do 2 apply bi.forall_intro=>?.
--
GitLab