diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 14a4b4e5358785fe79e251db6be6b8ec3d919e9f..9b3c212fc4361d93a6ce32631fdc1821e9ef7030 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -835,8 +835,9 @@ Arguments exist_split {_} _ _ {_}.
Global Instance exist_split_exist {A} (Φ: A → uPred M): ExistSplit (∃ a, Φ a) Φ.
Proof. done. Qed.
-Lemma tac_exist {A} Δ P (Φ : A → uPred M) a : ExistSplit P Φ → Δ ⊢ Φ a → Δ ⊢ P.
-Proof. intros. rewrite -(exist_split P). eauto using exist_intro'. Qed.
+Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
+ ExistSplit P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
+Proof. intros ? [a ?]. rewrite -(exist_split P). eauto using exist_intro'. Qed.
Class ExistDestruct {A} (P : uPred M) (Φ : A → uPred M) :=
exist_destruct : P ⊢ (∃ x, Φ x).
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 8191b3ff9f8ba656d0e07f52fa4abac8629d3b92..beb2db7a532e99edb32899b3c0f0190decff7208 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -506,34 +506,31 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
|env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
(** * Existential *)
-Tactic Notation "iExists" open_constr(x1) :=
- eapply tac_exist with _ x1 ;
+Tactic Notation "iExists" uconstr(x1) :=
+ eapply tac_exist;
[let P := match goal with |- ExistSplit ?P _ => P end in
apply _ || fail "iExists:" P "not an existential"
- |cbv beta].
+ |cbv beta; eexists x1].
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) :=
iExists x1; iExists x2.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
- open_constr(x3) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) :=
iExists x1; iExists x2, x3.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
- open_constr(x3) "," open_constr(x4) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+ uconstr(x4) :=
iExists x1; iExists x2, x3, x4.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
- open_constr(x3) "," open_constr(x4) "," open_constr(x5) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+ uconstr(x4) "," uconstr(x5) :=
iExists x1; iExists x2, x3, x4, x5.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
- open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
- open_constr(x6) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+ uconstr(x4) "," uconstr(x5) "," uconstr(x6) :=
iExists x1; iExists x2, x3, x4, x5, x6.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
- open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
- open_constr(x6) "," open_constr(x7) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+ uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) :=
iExists x1; iExists x2, x3, x4, x5, x6, x7.
-Tactic Notation "iExists" open_constr(x1) "," open_constr(x2) ","
- open_constr(x3) "," open_constr(x4) "," open_constr(x5) ","
- open_constr(x6) "," open_constr(x7) "," open_constr(x8) :=
+Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
+ uconstr(x4) "," uconstr(x5) "," uconstr(x6) "," uconstr(x7) ","
+ uconstr(x8) :=
iExists x1; iExists x2, x3, x4, x5, x6, x7, x8.
Tactic Notation "iExistDestruct" constr(H) "as" ident(x) constr(Hx) :=