Port `tac_specialize_assert`.

theories/proofmode/coq_tactics.v

@@ -270,16 +270,24 @@ Proof.
   - by rewrite HR assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert Δ Δ1 Δ2' j q neg js R P1 P2 P1' Q :
+Lemma tac_specialize_assert Δ j q neg js R P1 P2 P1' Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand q false R P1 P2 → AddModal P1' P1 Q →
-  (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left)
-      js (envs_delete true j q Δ);
+  match
+    ''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left)
+    js (envs_delete true j q Δ);
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
-    Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.
+    Some (Δ1,Δ2') (* does not preserve position of [j] *)
+  with
+  | Some (Δ1,Δ2') =>
+     (* The constructor [conj] of [∧] still stores the contexts [Δ1] and [Δ2'] *)
+     envs_entails Δ1 P1' ∧ envs_entails Δ2' Q
+  | None => False
+  end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? HP1 HQ.
+  rewrite envs_entails_eq. intros ??? HQ.
+  destruct (_ ≫= _) as [[Δ1 Δ2']|] eqn:?; last done.
+  destruct HQ as [HP1 HQ].
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.

theories/proofmode/ltac_tactics.v

@@ -851,7 +851,7 @@ Ltac iSpecializePat_go H1 pats :=
        fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
-       notypeclasses refine (tac_specialize_assert _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -860,11 +860,16 @@ Ltac iSpecializePat_go H1 pats :=
           | GSpatial => class_apply add_modal_id
           | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
           end
-         |pm_reflexivity ||
-          let Hs' := iMissingHyps Hs' in
-          fail "iSpecialize: hypotheses" Hs' "not found"
-         |iFrame Hs_frame; solve_done d (*goal*)
-         |iSpecializePat_go H1 pats]
+         |pm_reduce;
+          lazymatch goal with
+          | |- False =>
+            let Hs' := iMissingHyps Hs' in
+            fail "iSpecialize: hypotheses" Hs' "not found"
+          | _ =>
+            split;
+              [iFrame Hs_frame; solve_done d (*goal*)
+              |iSpecializePat_go H1 pats]
+          end]
     | SAutoFrame GIntuitionistic :: ?pats =>
        notypeclasses refine (tac_specialize_assert_intuitionistic _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||