Extend ElimModal with Boolean flags to specify whether it operates on the...

Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context.

theories/base_logic/lib/cancelable_invariants.v

@@ -93,12 +93,12 @@ Section proofs.
 
   Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
   Global Instance elim_inv_cinv p γ E N P Q Q' :
-    (∀ R, ElimModal True (|={E,E∖↑N}=> R) R Q Q') →
+    (∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
     ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p)
       (▷ P ∗ cinv_own γ p) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
   Proof.
     rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
-    iApply Helim; [done|]. iSplitR "H2"; [|done].
+    iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
     iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
     by iFrame.
   Qed.

theories/base_logic/lib/invariants.v

@@ -110,11 +110,11 @@ Qed.
 Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
 Global Instance elim_inv_inv E N P Q Q' :
-  (∀ R, ElimModal True (|={E,E∖↑N}=> R) R Q Q') →
+  (∀ R, ElimModal True false false (|={E,E∖↑N}=> R) R Q Q') →
   ElimInv (↑N ⊆ E) (inv N P) True (▷ P) (▷ P ={E∖↑N,E}=∗ True) Q Q'.
 Proof.
   rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
-  iApply (Helim with "[H2]"); [done|]. iSplitR "H2"; [|done].
+  iApply (Helim with "[H2]"); [done|]; simpl. iSplitR "H2"; [|done].
   iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
 Qed.
 

theories/base_logic/lib/na_invariants.v

@@ -113,12 +113,12 @@ Section proofs.
 
   Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
   Global Instance elim_inv_na p F E N P Q Q':
-    (∀ R, ElimModal True (|={E}=> R)%I R Q Q') →
+    (∀ R, ElimModal True false false (|={E}=> R)%I R Q Q') →
     ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F)
       (▷ P ∗ na_own p (F∖↑N)) (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F) Q Q'.
   Proof.
     rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
-    iApply Helim; [done|]. iSplitR "H2"; [|done].
+    iApply Helim; [done|]; simpl. iSplitR "H2"; [|done].
     iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
     by iFrame.
   Qed.

theories/bi/lib/counter_examples.v

@@ -29,8 +29,11 @@ Module savedprop. Section savedprop.
 
   Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
   Proof. intros P Q ?. by apply bupd_mono. Qed.
-  Instance elim_modal_bupd P Q : ElimModal True (|==> P) P (|==> Q) (|==> Q).
-  Proof. by rewrite /ElimModal bupd_frame_r bi.wand_elim_r bupd_trans. Qed.
+  Instance elim_modal_bupd p P Q : ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
+  Proof.
+    by rewrite /ElimModal bi.intuitionistically_if_elim
+      bupd_frame_r bi.wand_elim_r bupd_trans.
+  Qed.
 
   (** A bad recursive reference: "Assertion with name [i] does not hold" *)
   Definition A (i : ident) : PROP := (∃ P, ¬ P ∗ saved i P)%I.
@@ -127,12 +130,18 @@ Module inv. Section inv.
   Lemma fupd_frame_r E P Q : fupd E P ∗ Q ⊢ fupd E (P ∗ Q).
   Proof. by rewrite comm fupd_frame_l comm. Qed.
 
-  Global Instance elim_fupd_fupd E P Q : ElimModal True (fupd E P) P (fupd E Q) (fupd E Q).
-  Proof. by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_fupd. Qed.
+  Global Instance elim_fupd_fupd p E P Q :
+    ElimModal True p false (fupd E P) P (fupd E Q) (fupd E Q).
+  Proof.
+    by rewrite /ElimModal bi.intuitionistically_if_elim
+      fupd_frame_r bi.wand_elim_r fupd_fupd.
+  Qed.
 
-  Global Instance elim_fupd0_fupd1 P Q : ElimModal True (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
+  Global Instance elim_fupd0_fupd1 p P Q :
+    ElimModal True p false (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
   Proof.
-    by rewrite /ElimModal fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
+    by rewrite /ElimModal bi.intuitionistically_if_elim
+      fupd_frame_r bi.wand_elim_r fupd_mask_mono fupd_fupd.
   Qed.
 
   Global Instance exists_split_fupd0 {A} E P (Φ : A → PROP) :

theories/program_logic/total_weakestpre.v

@@ -384,19 +384,28 @@ Section proofmode_classes.
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
   Proof. by rewrite /IsExcept0 -{2}fupd_twp -except_0_fupd -fupd_intro. Qed.
 
-  Global Instance elim_modal_bupd_twp s E e P Φ :
-    ElimModal True (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
-  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_twp. Qed.
+  Global Instance elim_modal_bupd_twp p s E e P Φ :
+    ElimModal True p false (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof.
+    by rewrite /ElimModal intuitionistically_if_elim
+      (bupd_fupd E) fupd_frame_r wand_elim_r fupd_twp.
+  Qed.
 
-  Global Instance elim_modal_fupd_twp s E e P Φ :
-    ElimModal True (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
-  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_twp. Qed.
+  Global Instance elim_modal_fupd_twp p s E e P Φ :
+    ElimModal True p false (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof.
+    by rewrite /ElimModal intuitionistically_if_elim
+      fupd_frame_r wand_elim_r fupd_twp.
+  Qed.
 
-  Global Instance elim_modal_fupd_twp_atomic s E1 E2 e P Φ :
+  Global Instance elim_modal_fupd_twp_atomic p s E1 E2 e P Φ :
     Atomic (stuckness_to_atomicity s) e →
-    ElimModal True (|={E1,E2}=> P) P
+    ElimModal True p false (|={E1,E2}=> P) P
             (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
-  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r twp_atomic. Qed.
+  Proof.
+    intros. by rewrite /ElimModal intuitionistically_if_elim
+      fupd_frame_r wand_elim_r twp_atomic.
+  Qed.
 
   Global Instance add_modal_fupd_twp s E e P Φ :
     AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).

theories/program_logic/weakestpre.v

@@ -378,19 +378,28 @@ Section proofmode_classes.
   Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E {{ Φ }}).
   Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
 
-  Global Instance elim_modal_bupd_wp s E e P Φ :
-    ElimModal True (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
-  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
-
-  Global Instance elim_modal_fupd_wp s E e P Φ :
-    ElimModal True (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
-  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
-
-  Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
+  Global Instance elim_modal_bupd_wp p s E e P Φ :
+    ElimModal True p false (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
+  Proof.
+    by rewrite /ElimModal intuitionistically_if_elim
+      (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp.
+  Qed.
+
+  Global Instance elim_modal_fupd_wp p s E e P Φ :
+    ElimModal True p false (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
+  Proof.
+    by rewrite /ElimModal intuitionistically_if_elim
+      fupd_frame_r wand_elim_r fupd_wp.
+  Qed.
+
+  Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
     Atomic (stuckness_to_atomicity s) e →
-    ElimModal True (|={E1,E2}=> P) P
+    ElimModal True p false (|={E1,E2}=> P) P
             (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
-  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
+  Proof.
+    intros. by rewrite /ElimModal intuitionistically_if_elim
+      fupd_frame_r wand_elim_r wp_atomic.
+  Qed.
 
   Global Instance add_modal_fupd_wp s E e P Φ :
     AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).

theories/proofmode/class_instances_bi.v

@@ -763,37 +763,40 @@ Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
   IntoInv P N → IntoInv ⎡P⎤ N.
 
 (* ElimModal *)
-Global Instance elim_modal_wand φ P P' Q Q' R :
-  ElimModal φ P P' Q Q' → ElimModal φ P P' (R -∗ Q) (R -∗ Q').
+Global Instance elim_modal_wand φ p p' P P' Q Q' R :
+  ElimModal φ p p' P P' Q Q' → ElimModal φ p p' P P' (R -∗ Q) (R -∗ Q').
 Proof.
   rewrite /ElimModal=> H Hφ. apply wand_intro_r.
-  rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l; auto.
+  rewrite wand_curry -assoc (comm _ (□?p' _)%I) -wand_curry wand_elim_l; auto.
 Qed.
-Global Instance elim_modal_forall {A} φ P P' (Φ Ψ : A → PROP) :
-  (∀ x, ElimModal φ P P' (Φ x) (Ψ x)) → ElimModal φ P P' (∀ x, Φ x) (∀ x, Ψ x).
+Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A → PROP) :
+  (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) → ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
   rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
 Qed.
-Global Instance elim_modal_absorbingly_here P Q :
-  Absorbing Q → ElimModal True (<absorb> P) P Q Q.
+Global Instance elim_modal_absorbingly_here p P Q :
+  Absorbing Q → ElimModal True p false (<absorb> P) P Q Q.
 Proof.
-  rewrite /ElimModal=> H.
-  by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
+  rewrite /ElimModal=> ? _. by rewrite intuitionistically_if_elim
+    absorbingly_sep_l wand_elim_r absorbing_absorbingly.
 Qed.
 
-Global Instance elim_modal_bupd `{BiBUpd PROP} P Q :
-  ElimModal True (|==> P) P (|==> Q) (|==> Q).
-Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
+Global Instance elim_modal_bupd `{BiBUpd PROP} p P Q :
+  ElimModal True p false (|==> P) P (|==> Q) (|==> Q).
+Proof.
+  by rewrite /ElimModal
+    intuitionistically_if_elim bupd_frame_r wand_elim_r bupd_trans.
+Qed.
 
 Global Instance elim_modal_embed_bupd_goal `{BiEmbedBUpd PROP PROP'}
-       φ (P P' : PROP') (Q Q' : PROP) :
-  ElimModal φ P P' (|==> ⎡Q⎤)%I (|==> ⎡Q'⎤)%I →
-  ElimModal φ P P' ⎡|==> Q⎤ ⎡|==> Q'⎤.
+    p p' φ (P P' : PROP') (Q Q' : PROP) :
+  ElimModal φ p p' P P' (|==> ⎡Q⎤)%I (|==> ⎡Q'⎤)%I →
+  ElimModal φ p p' P P' ⎡|==> Q⎤ ⎡|==> Q'⎤.
 Proof. by rewrite /ElimModal !embed_bupd. Qed.
 Global Instance elim_modal_embed_bupd_hyp `{BiEmbedBUpd PROP PROP'}
-       φ (P : PROP) (P' Q Q' : PROP') :
-  ElimModal φ (|==> ⎡P⎤)%I P' Q Q' →
-  ElimModal φ ⎡|==> P⎤ P' Q Q'.
+    p p' φ (P : PROP) (P' Q Q' : PROP') :
+  ElimModal φ p p' (|==> ⎡P⎤)%I P' Q Q' →
+  ElimModal φ p p' ⎡|==> P⎤ P' Q Q'.
 Proof. by rewrite /ElimModal !embed_bupd. Qed.
 
 (* AddModal *)

theories/proofmode/class_instances_sbi.v

@@ -474,38 +474,45 @@ Global Instance into_except_0_embed `{SbiEmbed PROP PROP'} P Q :
 Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
 
 (* ElimModal *)
-Global Instance elim_modal_timeless P Q :
-  IntoExcept0 P P' → IsExcept0 Q → ElimModal True P P' Q Q.
+Global Instance elim_modal_timeless p P Q :
+  IntoExcept0 P P' → IsExcept0 Q → ElimModal True p p P P' Q Q.
 Proof.
-  intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I).
-  by rewrite (into_except_0 P) -except_0_sep wand_elim_r.
+  intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I) (into_except_0 P).
+  by rewrite except_0_intuitionistically_if_2 -except_0_sep wand_elim_r.
 Qed.
 
-Global Instance elim_modal_bupd_plain_goal `{BiBUpdPlainly PROP} P Q :
-  Plain Q → ElimModal True (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
-Global Instance elim_modal_bupd_plain `{BiBUpdPlainly PROP} P Q :
-  Plain P → ElimModal True (|==> P) P Q Q.
+Global Instance elim_modal_bupd_plain_goal `{BiBUpdPlainly PROP} p P Q :
+  Plain Q → ElimModal True p false (|==> P) P Q Q.
+Proof.
+  intros. by rewrite /ElimModal intuitionistically_if_elim
+    bupd_frame_r wand_elim_r bupd_plain.
+Qed.
+Global Instance elim_modal_bupd_plain `{BiBUpdPlainly PROP} p P Q :
+  Plain P → ElimModal True p p (|==> P) P Q Q.
 Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
-Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} E1 E2 P Q :
-  ElimModal True (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
+Global Instance elim_modal_bupd_fupd `{BiBUpdFUpd PROP} p E1 E2 P Q :
+  ElimModal True p false (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
 Proof.
-  by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
+  by rewrite /ElimModal intuitionistically_if_elim
+    (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
 Qed.
 
-Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} E1 E2 E3 P Q :
-  ElimModal True (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
-Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
+Global Instance elim_modal_fupd_fupd `{BiFUpd PROP} p E1 E2 E3 P Q :
+  ElimModal True p false (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+Proof.
+  by rewrite /ElimModal intuitionistically_if_elim
+    fupd_frame_r wand_elim_r fupd_trans.
+Qed.
 
 Global Instance elim_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
-       φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
-  ElimModal φ P P' (|={E1,E3}=> ⎡Q⎤)%I (|={E2,E3}=> ⎡Q'⎤)%I →
-  ElimModal φ P P' ⎡|={E1,E3}=> Q⎤ ⎡|={E2,E3}=> Q'⎤.
+    p p' φ E1 E2 E3 (P P' : PROP') (Q Q' : PROP) :
+  ElimModal φ p p' P P' (|={E1,E3}=> ⎡Q⎤)%I (|={E2,E3}=> ⎡Q'⎤)%I →
+  ElimModal φ p p' P P' ⎡|={E1,E3}=> Q⎤ ⎡|={E2,E3}=> Q'⎤.
 Proof. by rewrite /ElimModal !embed_fupd. Qed.
 Global Instance elim_modal_embed_fupd_hyp `{BiEmbedFUpd PROP PROP'}
-       φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
-  ElimModal φ (|={E1,E2}=> ⎡P⎤)%I P' Q Q' →
-  ElimModal φ ⎡|={E1,E2}=> P⎤ P' Q Q'.
+    p p' φ E1 E2 (P : PROP) (P' Q Q' : PROP') :
+  ElimModal φ p p' (|={E1,E2}=> ⎡P⎤)%I P' Q Q' →
+  ElimModal φ p p' ⎡|={E1,E2}=> P⎤ P' Q Q'.
 Proof. by rewrite /ElimModal embed_fupd. Qed.
 
 (* AddModal *)

theories/proofmode/classes.v

@@ -234,11 +234,11 @@ Arguments IsExcept0 {_} _%I : simpl never.
 Arguments is_except_0 {_} _%I {_}.
 Hint Mode IsExcept0 + ! : typeclass_instances.
 
-Class ElimModal {PROP : bi} (φ : Prop) (P P' : PROP) (Q Q' : PROP) :=
-  elim_modal : φ → P ∗ (P' -∗ Q') ⊢ Q.
-Arguments ElimModal {_} _ _%I _%I _%I _%I : simpl never.
-Arguments elim_modal {_} _ _%I _%I _%I _%I {_}.
-Hint Mode ElimModal + - ! - ! - : typeclass_instances.
+Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
+  elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.
+Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
+Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
+Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
 
 (* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
 add a modality to the goal corresponding to a premise/asserted proposition. *)
@@ -556,8 +556,8 @@ Instance into_forall_tc_opaque {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
 Instance from_modal_tc_opaque {PROP1 PROP2 : bi} {A}
     M (sel : A) (P : PROP2) (Q : PROP1) :
   FromModal M sel P Q → FromModal M sel (tc_opaque P) Q := id.
-Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
-  ElimModal φ P P' Q Q' → ElimModal φ (tc_opaque P) P' Q Q' := id.
+Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
+  ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
 Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
   IntoInv P N → IntoInv (tc_opaque P) N := id.
 Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Pclose Q Q' : PROP) :

theories/proofmode/coq_tactics.v

@@ -1054,15 +1054,15 @@ Proof.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_elim Δ Δ' i p φ P' P Q Q' :
+Lemma tac_modal_elim Δ Δ' i p p' φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
-  ElimModal φ P P' Q Q' →
+  ElimModal φ p p' P P' Q Q' →
   φ →
-  envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' →
+  envs_replace i p p' (Esnoc Enil i P') Δ = Some Δ' →
   envs_entails Δ' Q' → envs_entails Δ Q.
 Proof.
   rewrite envs_entails_eq => ???? HΔ. rewrite envs_replace_singleton_sound //=.
-  rewrite HΔ intuitionistically_if_elim. by eapply elim_modal.
+  rewrite HΔ. by eapply elim_modal.
 Qed.
 
 (** * Invariants *)

theories/proofmode/monpred.v

@@ -359,14 +359,14 @@ Proof.
   by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
 Qed.
 
-Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q Q' i :
-  ElimModal φ 𝓟 𝓟' (|==> Q i) (|==> Q' i) →
-  ElimModal φ 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
+Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ p p' 𝓟 𝓟' Q Q' i :
+  ElimModal φ p p' 𝓟 𝓟' (|==> Q i) (|==> Q' i) →
+  ElimModal φ p p' 𝓟 𝓟' ((|==> Q) i) ((|==> Q') i).
 Proof. by rewrite /ElimModal !monPred_at_bupd. Qed.
-Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ P 𝓟 𝓟' 𝓠 𝓠' i:
+Global Instance elim_modal_at_bupd_hyp `{BiBUpd PROP} φ p p' P 𝓟 𝓟' 𝓠 𝓠' i:
   MakeMonPredAt i P 𝓟 →
-  ElimModal φ (|==> 𝓟) 𝓟' 𝓠 𝓠' →
-  ElimModal φ ((|==> P) i) 𝓟' 𝓠 𝓠'.
+  ElimModal φ p p' (|==> 𝓟) 𝓟' 𝓠 𝓠' →
+  ElimModal φ p p' ((|==> P) i) 𝓟' 𝓠 𝓠'.
 Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_bupd=><-. Qed.
 
 Global Instance add_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q i :
@@ -465,14 +465,14 @@ Proof.
   by rewrite monPred_at_later.
 Qed.
 
-Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ E1 E2 E3 𝓟 𝓟' Q Q' i :
-  ElimModal φ 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
-  ElimModal φ 𝓟 𝓟' ((|={E1,E3}=> Q) i) ((|={E2,E3}=> Q') i).
+Global Instance elim_modal_at_fupd_goal `{BiFUpd PROP} φ p p' E1 E2 E3 𝓟 𝓟' Q Q' i :
+  ElimModal φ p p' 𝓟 𝓟' (|={E1,E3}=> Q i) (|={E2,E3}=> Q' i) →
+  ElimModal φ p p' 𝓟 𝓟' ((|={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 :
+Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟' 𝓠 𝓠' i :
   MakeMonPredAt i P 𝓟 →
-  ElimModal φ (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠' →
-  ElimModal φ ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
+  ElimModal φ p p' (|={E1,E2}=> 𝓟) 𝓟' 𝓠 𝓠' →
+  ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
 Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
 
 Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :

theories/proofmode/tactics.v

@@ -1012,11 +1012,11 @@ Tactic Notation "iNext" := iModIntro (▷^_ _)%I.
 
 (** * Update modality *)
 Tactic Notation "iModCore" constr(H) :=
-  eapply tac_modal_elim with _ H _ _ _ _ _;
+  eapply tac_modal_elim with _ H _ _ _ _ _ _;
     [env_reflexivity || fail "iMod:" H "not found"
     |iSolveTC ||
-     let P := match goal with |- ElimModal _ ?P _ _ _ => P end in
-     let Q := match goal with |- ElimModal _ _ _ ?Q _ => Q end in
+     let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in
+     let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
      fail "iMod: cannot eliminate modality " P "in" Q
     |try fast_done (* optional side-condition *)
     |env_reflexivity|].