From 4eb6e55d9b2058cd92f9bdba358b184f237e5c5c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 16 Jan 2018 18:31:13 +0100
Subject: [PATCH] AddModal instances for except0 and later, to recover the old
 behavior

---
 theories/proofmode/class_instances.v | 30 +++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 415ab1c1f..546c65c07 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -868,16 +868,16 @@ Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)).
   by rewrite -except_0_sep wand_elim_r.
 Qed.
-Global Instance elim_modal_timeless_bupd P Q :
+Global Instance elim_modal_later_timeless P Q :
   Timeless P → IsExcept0 Q → ElimModal (▷ P) P Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (timeless P).
   by rewrite -except_0_sep wand_elim_r.
 Qed.
-Global Instance elim_modal_timeless_bupd' p P Q :
+Global Instance elim_modal_later_if_timeless p P Q :
   Timeless P → IsExcept0 Q → ElimModal (▷?p P) P Q Q.
 Proof.
-  destruct p; simpl; auto using elim_modal_timeless_bupd.
+  destruct p; simpl; auto using elim_modal_later_timeless.
   intros _ _. by rewrite /ElimModal wand_elim_r.
 Qed.
 
@@ -896,6 +896,30 @@ Qed.
 Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
 Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 
+(* High priority to add a â–· rather than a â—‡ when P is timeless. *)
+Global Instance add_modal_later_except_0 P Q :
+  Timeless P → AddModal (▷ P) P (◇ Q) | 0.
+Proof.
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
+  by rewrite -except_0_sep wand_elim_r except_0_idemp.
+Qed.
+Global Instance add_modal_later P Q :
+  Timeless P → AddModal (▷ P) P (▷ Q) | 0.
+Proof.
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
+  by rewrite -except_0_sep wand_elim_r except_0_later.
+Qed.
+Global Instance add_modal_except_0 P Q : AddModal (â—‡ P) P (â—‡ Q).
+Proof.
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
+  by rewrite -except_0_sep wand_elim_r except_0_idemp.
+Qed.
+Global Instance add_modal_except_0_later P Q : AddModal (â—‡ P) P (â–· Q).
+Proof.
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
+  by rewrite -except_0_sep wand_elim_r except_0_later.
+Qed.
+
 (** IsExcept0 *)
 Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
-- 
GitLab