Port `tac_specialize`.

theories/proofmode/coq_tactics.v

@@ -250,9 +250,9 @@ Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
-(* TODO: convert to not take Δ' *)
-Lemma tac_specialize remove_intuitionistic Δ Δ' i p j q P1 P2 R Q :
-  envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') →
+Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
+  envs_lookup i Δ = Some (p, P1) →
+  let Δ' := envs_delete remove_intuitionistic i p Δ in
   envs_lookup j Δ' = Some (q, R) →
   IntoWand q p R P1 P2 →
   match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
@@ -260,8 +260,7 @@ Lemma tac_specialize remove_intuitionistic Δ Δ' i p j q P1 P2 R Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq /IntoWand.
-  intros [? ->]%envs_lookup_delete_Some ? HR ?.
+  rewrite envs_entails_eq /IntoWand. intros ?? HR ?.
   destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
   rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
   rewrite envs_replace_singleton_sound //. destruct p; simpl in *.

theories/proofmode/ltac_tactics.v

@@ -784,7 +784,7 @@ Ltac iSpecializePat_go H1 pats :=
     | SIdent ?H2 [] :: ?pats =>
        (* If we not need to specialize [H2] we can avoid a lot of unncessary
        context manipulation. *)
-       notypeclasses refine (tac_specialize false _ _ H2 _ H1 _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize false _ H2 _ H1 _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H2 := pretty_ident H2 in
           fail "iSpecialize:" H2 "not found"
@@ -811,7 +811,7 @@ Ltac iSpecializePat_go H1 pats :=
          Ltac backtraces (which would otherwise include the whole closure). *)
          [.. (* side-conditions of [iSpecialize] *)
          |(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *)
-          notypeclasses refine (tac_specialize true _ _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
+          notypeclasses refine (tac_specialize true _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
             [pm_reflexivity ||
              let H2tmp := pretty_ident H2tmp in
              fail "iSpecialize:" H2tmp "not found"