From e8652bfafa025e0886d7d1a7e04a8866a2a8e442 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Dec 2019 12:26:19 +0100
Subject: [PATCH] Make handling of `AddModal` in `tac_specialize_frame`
 consistent with that in `tac_specialize_assert`.

---
 theories/proofmode/coq_tactics.v  | 10 +++++-----
 theories/proofmode/ltac_tactics.v |  8 +++-----
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 5720969d2..50d3c6988 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -326,18 +326,18 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
 Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
-Lemma tac_specialize_frame Δ j q R P1 P2 P1' Q Q' :
+Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
   envs_lookup j Δ = Some (q, R) →
   IntoWand q false R P1 P2 →
-  AddModal P1' P1 Q →
+  (if am then AddModal P1' P1 Q else TCEq P1' P1) →
   envs_entails (envs_delete true j q Δ) (P1' ∗ locked Q') →
   Q' = (P2 -∗ Q)%I →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ??? HPQ ->.
+  rewrite envs_entails_eq. intros ?? Hmod HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
-  rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
-  apply wand_intro_l. by rewrite assoc !wand_elim_r.
+  rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
+  destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
 Qed.
 
 Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index db77fe7dd..d1d785a89 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -932,15 +932,13 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reduce; solve [iFrame "∗ #"]
          |pm_reduce; iSpecializePat_go H1 pats]
     | SAutoFrame ?m :: ?pats =>
-       notypeclasses refine (tac_specialize_frame _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_frame _ H1 _
+           (if m is GModal then true else false) _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
          |solve_to_wand H1
-         |lazymatch m with
-          | GSpatial => class_apply add_modal_id
-          | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
-          end
+         |iSolveTC || fail "iSpecialize: goal not a modality"
          |pm_reduce;
           first
             [notypeclasses refine (tac_unlock_emp _ _ _)
-- 
GitLab