Remove context duplication from tac_exist_destruct.

theories/proofmode/coq_tactics.v

@@ -631,14 +631,17 @@ Qed.
 
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) Q :
   envs_lookup i Δ = Some (p, P) → IntoExist P Φ →
-  (∀ a, ∃ Δ',
-    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧
-    envs_entails Δ' Q) →
+  (∀ a,
+    match envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ with
+    | Some Δ' => envs_entails Δ' Q
+    | None => False
+    end) →
   envs_entails Δ Q.
 Proof.
   rewrite envs_entails_eq => ?? HΦ. rewrite envs_lookup_sound //.
   rewrite (into_exist P) intuitionistically_if_exist sep_exist_r.
-  apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
+  apply exist_elim=> a; specialize (HΦ a) as Hmatch.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
   rewrite envs_simple_replace_singleton_sound' //; simpl. by rewrite wand_elim_r.
 Qed.
 

theories/proofmode/ltac_tactics.v

@@ -1232,13 +1232,14 @@ Local Tactic Notation "iExistDestruct" constr(H)
     |iSolveTC ||
      let P := match goal with |- IntoExist ?P _ => P end in
      fail "iExistDestruct: cannot destruct" P|];
-  let y := fresh in
-  intros y; eexists; split;
-    [pm_reflexivity ||
-     let Hx := pretty_ident Hx in
-     fail "iExistDestruct:" Hx "not fresh"
-    |revert y; intros x
-     (* subgoal *)].
+    let y := fresh in
+    intros y; pm_reduce;
+    match goal with
+    | |- False =>
+      let Hx := pretty_ident Hx in
+      fail "iExistDestruct:" Hx "not fresh"
+    | _ => revert y; intros x (* subgoal *)
+    end.
 
 (** * Modality introduction *)
 Tactic Notation "iModIntro" uconstr(sel) :=