Fix error message regression, add new test cases.

Also fixes pre-existing bug in iCombine error messages.

tests/proofmode.ref

@@ -456,7 +456,7 @@ The command has indeed failed with message:
 In nested Ltac calls to "iIntros ( (intropattern) )",
 "iIntro ( (intropattern) )" and "intros x", last call failed.
 x is already used.
-"iSplit_one_of_many"
+"iSplitL_one_of_many"
      : string
 The command has indeed failed with message:
 Ltac call to "iSplitL (constr)" failed.
@@ -464,6 +464,39 @@ Tactic failure: iSplitL: hypotheses ["HPx"] not found.
 The command has indeed failed with message:
 Ltac call to "iSplitL (constr)" failed.
 Tactic failure: iSplitL: hypotheses ["HPx"] not found.
+"iSplitR_one_of_many"
+     : string
+The command has indeed failed with message:
+Ltac call to "iSplitR (constr)" failed.
+Tactic failure: iSplitR: hypotheses ["HPx"] not found.
+The command has indeed failed with message:
+Ltac call to "iSplitR (constr)" failed.
+Tactic failure: iSplitR: hypotheses ["HPx"] not found.
+"iCombine_fail"
+     : string
+The command has indeed failed with message:
+Ltac call to "iCombine (constr) as (constr)" failed.
+Tactic failure: iCombine: hypotheses ["HP3"] not found.
+"iSpecialize_bad_name1_fail"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
+failed.
+Tactic failure: iSpecialize: "H" not found.
+"iSpecialize_bad_name2_fail"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iSpecialize (open_constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) as (constr)",
+"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
+"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
+failed.
+Tactic failure: iSpecialize: "H" not found.
 "iExact_fail"
      : string
 The command has indeed failed with message:
@@ -519,12 +552,30 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
 "iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
 "iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
 "tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "tac" (bound to fun H => iDestructHyp H as pat),
 "iDestructHyp (constr) as (constr)",
 "<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
 "<iris.proofmode.ltac_tactics.iDestructHypGo>" and
 "iRename (constr) into (constr)", last call failed.
 Tactic failure: iRename: "H" not fresh.
+"iPoseProof_not_found_fail"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
+"iPoseProofCoreHyp (constr) as (constr)", last call failed.
+Tactic failure: iPoseProof: "Hx" not found.
+"iPoseProofCoreHyp_not_found_fail"
+     : string
+The command has indeed failed with message:
+Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
+Tactic failure: iPoseProof: "Hx" not found.
+"iPoseProofCoreHyp_not_fresh_fail"
+     : string
+The command has indeed failed with message:
+Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
+Tactic failure: iPoseProof: "H1" not fresh.
 "iRevert_fail"
      : string
 The command has indeed failed with message:
@@ -555,6 +606,14 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)",
 "<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
 Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
 invalid.
+"iOrDestruct_fail"
+     : string
+The command has indeed failed with message:
+Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
+Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
+The command has indeed failed with message:
+Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
+Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
 "iApply_fail"
      : string
 The command has indeed failed with message:

tests/proofmode.v

@@ -777,13 +777,41 @@ Proof.
   iIntros "HQ" (x). Fail iIntros (x).
 Abort.
 
-Check "iSplit_one_of_many".
-Lemma iSplit_one_of_many P :
+Check "iSplitL_one_of_many".
+Lemma iSplitL_one_of_many P :
   P -∗ P -∗ P ∗ P.
 Proof.
   iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
 Abort.
 
+Check "iSplitR_one_of_many".
+Lemma iSplitR_one_of_many P :
+  P -∗ P -∗ P ∗ P.
+Proof.
+  iIntros "HP1 HP2". Fail iSplitR "HP1 HPx". Fail iSplitR "HPx HP1".
+Abort.
+
+Check "iCombine_fail".
+Lemma iCombine_fail P:
+  P -∗ P -∗ P ∗ P.
+Proof.
+  iIntros "HP1 HP2". Fail iCombine "HP1 HP3" as "HP".
+Abort.
+
+Check "iSpecialize_bad_name1_fail".
+Lemma iSpecialize_bad_name1_fail P Q:
+  (P -∗ Q) -∗ P -∗ Q.
+Proof.
+  iIntros "HW HP". Fail iSpecialize ("H" with "HP").
+Abort.
+
+Check "iSpecialize_bad_name2_fail".
+Lemma iSpecialize_bad_name2_fail P Q:
+  (P -∗ Q) -∗ P -∗ Q.
+Proof.
+  iIntros "HW HP". Fail iSpecialize ("HW" with "H").
+Abort.
+
 Check "iExact_fail".
 Lemma iExact_fail P Q :
   <affine> P -∗ Q -∗ <affine> P.
@@ -811,6 +839,24 @@ Proof.
   iIntros "H". Fail iPoseProof bi.and_intro as "H".
 Abort.
 
+Check "iPoseProof_not_found_fail".
+Lemma iPoseProof_not_found_fail P : P -∗ P.
+Proof.
+  iIntros "H". Fail iPoseProof "Hx" as "H1".
+Abort.
+
+Check "iPoseProofCoreHyp_not_found_fail".
+Lemma iPoseProofCoreHyp_not_found_fail P : P -∗ P -∗ P.
+Proof.
+  iIntros "H". Fail iPoseProofCoreHyp "Hx" as "H1".
+Abort.
+
+Check "iPoseProofCoreHyp_not_fresh_fail".
+Lemma iPoseProofCoreHyp_not_fresh_fail P : P -∗ P -∗ P.
+Proof.
+  iIntros "H0 H1". Fail iPoseProofCoreHyp "H0" as "H1".
+Abort.
+
 Check "iRevert_fail".
 Lemma iRevert_fail P : P -∗ P.
 Proof. Fail iRevert "H". Abort.
@@ -819,6 +865,12 @@ Check "iDestruct_fail".
 Lemma iDestruct_fail P : P -∗ <absorb> P.
 Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.
 
+Check "iOrDestruct_fail".
+Lemma iOrDestruct_fail P : (P ∨ P) -∗ P -∗ P.
+Proof.
+  iIntros "H H'". Fail iOrDestruct "H" as "H'" "H2". Fail iOrDestruct "H" as "H1" "H'".
+Abort.
+
 Check "iApply_fail".
 Lemma iApply_fail P Q : P -∗ Q.
 Proof. iIntros "HP". Fail iApply "HP". Abort.

theories/proofmode/ltac_tactics.v

@@ -39,15 +39,20 @@ Ltac pretty_ident H :=
 
 (** * Misc *)
 
-Ltac iMissingHyps Hs :=
-  let Δ :=
-    lazymatch goal with
-    | |- envs_entails ?Δ _ => Δ
-    | |- context[ envs_split _ _ ?Δ ] => Δ
-    end in
+Ltac iGetCtx :=
+  lazymatch goal with
+  | |- envs_entails ?Δ _ => Δ
+  | |- context[ envs_split _ _ ?Δ ] => Δ
+  end.
+
+Ltac iMissingHypsCore Δ Hs :=
   let Hhyps := pm_eval (envs_dom Δ) in
   eval vm_compute in (list_difference Hs Hhyps).
 
+Ltac iMissingHyps Hs :=
+  let Δ := iGetCtx in
+  iMissingHypsCore Δ Hs.
+
 Ltac iTypeOf H :=
   let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
   pm_eval (envs_lookup H Δ).
@@ -119,13 +124,17 @@ Ltac iFresh :=
 
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
-  eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
+  eapply tac_rename with H1 H2 _ _; (* (i:=H1) (j:=H2) *)
     [pm_reflexivity ||
      let H1 := pretty_ident H1 in
      fail "iRename:" H1 "not found"
-    |pm_reflexivity ||
-     let H2 := pretty_ident H2 in
-     fail "iRename:" H2 "not fresh"|].
+    |pm_reduce;
+     lazymatch goal with
+       | |- False =>
+         let H2 := pretty_ident H2 in
+         fail "iRename:" H2 "not fresh"
+       | _ => idtac (* subgoal *)
+     end].
 
 (** Elaborated selection patterns, unlike the type [sel_pat], contains
 only specific identifiers, and no wildcards like `#` (with the
@@ -197,11 +206,10 @@ Local Ltac iEval_go t Hs :=
   | [] => idtac
   | ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
   | ESelIdent _ ?H :: ?Hs =>
-    eapply tac_eval_in with _ H _ _ _;
+    eapply tac_eval_in with H _ _ _;
       [pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
       |let x := fresh in intros x; t; unfold x; reflexivity
-      |pm_reflexivity
-      |iEval_go t Hs]
+      |pm_reduce; iEval_go t Hs]
   end.
 
 Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
@@ -276,7 +284,7 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
 
 (** * Making hypotheses intuitionistic or pure *)
 Local Tactic Notation "iIntuitionistic" constr(H) :=
-  eapply tac_intuitionistic with _ H _ _ _; (* (i:=H) *)
+  eapply tac_intuitionistic with H _ _ _; (* (i:=H) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iIntuitionistic:" H "not found"
@@ -286,7 +294,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
     |pm_reduce; iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
      fail "iIntuitionistic:" P "not affine and the goal not absorbing"
-    |pm_reflexivity|].
+    |pm_reduce].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
@@ -448,41 +456,51 @@ Local Tactic Notation "iIntro" constr(H) :=
   iStartProof;
   first
   [(* (?Q → _) *)
-    eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
+    eapply tac_impl_intro with H _ _ _; (* (i:=H) *)
       [iSolveTC
       |pm_reduce; iSolveTC ||
        let P := lazymatch goal with |- Persistent ?P => P end in
        fail 1 "iIntro: introducing non-persistent" H ":" P
               "into non-empty spatial context"
-      |pm_reflexivity ||
-       let H := pretty_ident H in
-       fail 1 "iIntro:" H "not fresh"
       |iSolveTC
-      |(* subgoal *)]
+      |pm_reduce;
+       let H := pretty_ident H in
+        lazymatch goal with
+        | |- False =>
+          let H := pretty_ident H in
+          fail 1 "iIntro:" H "not fresh"
+        | _ => idtac (* subgoal *)
+        end]
   |(* (_ -∗ _) *)
-    eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
+    eapply tac_wand_intro with H _ _; (* (i:=H) *)
       [iSolveTC
-      | pm_reflexivity ||
-        let H := pretty_ident H in
-        fail 1 "iIntro:" H "not fresh"
-      |(* subgoal *)]
+      | pm_reduce;
+        lazymatch goal with
+        | |- False =>
+          let H := pretty_ident H in
+          fail 1 "iIntro:" H "not fresh"
+        | _ => idtac (* subgoal *)
+        end]
   | fail 1 "iIntro: nothing to introduce" ].
 
 Local Tactic Notation "iIntro" "#" constr(H) :=
   iStartProof;
   first
   [(* (?P → _) *)
-   eapply tac_impl_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
+   eapply tac_impl_intro_intuitionistic with H _ _ _; (* (i:=H) *)
      [iSolveTC
      |iSolveTC ||
       let P := match goal with |- IntoPersistent _ ?P _ => P end in
       fail 1 "iIntro:" P "not persistent"
-     |pm_reflexivity ||
-      let H := pretty_ident H in
-      fail 1 "iIntro:" H "not fresh"
-     |(* subgoal *)]
+     |pm_reduce;
+      lazymatch goal with
+      | |- False =>
+        let H := pretty_ident H in
+        fail 1 "iIntro:" H "not fresh"
+      | _ => idtac (* subgoal *)
+      end]
   |(* (?P -∗ _) *)
-   eapply tac_wand_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
+   eapply tac_wand_intro_intuitionistic with H _ _ _; (* (i:=H) *)
      [iSolveTC
      |iSolveTC ||
       let P := match goal with |- IntoPersistent _ ?P _ => P end in
@@ -490,10 +508,13 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
      |iSolveTC ||
       let P := match goal with |- TCOr (Affine ?P) _ => P end in
       fail 1 "iIntro:" P "not affine and the goal not absorbing"
-     |pm_reflexivity ||
-      let H := pretty_ident H in
-      fail 1 "iIntro:" H "not fresh"
-     |(* subgoal *)]
+     |pm_reduce;
+      lazymatch goal with
+      | |- False =>
+        let H := pretty_ident H in
+        fail 1 "iIntro:" H "not fresh"
+      | _ => idtac (* subgoal *)
+      end]
   |fail 1 "iIntro: nothing to introduce"].
 
 Local Tactic Notation "iIntro" constr(H) "as" constr(p) :=
@@ -686,23 +707,34 @@ Local Ltac iIntoEmpValid t :=
           |exact t]].
 
 Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
-  eapply tac_pose_proof_hyp with _ _ H _ Hnew _;
-    [pm_reflexivity ||
-     let H := pretty_ident H in
-     fail "iPoseProof:" H "not found"
-    |pm_reflexivity ||
-     let Htmp := pretty_ident Hnew in
-     fail "iPoseProof:" Hnew "not fresh"
-    |].
+  let Δ := iGetCtx in
+  eapply tac_pose_proof_hyp with H Hnew;
+    pm_reduce;
+    lazymatch goal with
+    | |- False =>
+      let lookup := pm_eval (envs_lookup_delete false H Δ) in
+      lazymatch lookup with
+      | None =>
+        let H := pretty_ident H in
+        fail "iPoseProof:" H "not found"
+      | _ =>
+        let Hnew := pretty_ident Hnew in
+        fail "iPoseProof:" Hnew "not fresh"
+      end
+    | _ => idtac
+    end.
 
 Tactic Notation "iPoseProofCoreLem"
     constr(lem) "as" constr(Hnew) "before_tc" tactic(tac) :=
-  eapply tac_pose_proof with _ Hnew _; (* (j:=H) *)
+  eapply tac_pose_proof with Hnew _; (* (j:=H) *)
     [iIntoEmpValid lem
-    |pm_reflexivity ||
-     let Htmp := pretty_ident Hnew in
-     fail "iPoseProof:" Hnew "not fresh"
-    |tac];
+    |pm_reduce;
+     lazymatch goal with
+     | |- False =>
+       let Hnew := pretty_ident Hnew in
+       fail "iPoseProof:" Hnew "not fresh"
+     | _ => tac
+     end];
   (* Solve all remaining TC premises generated by [iIntoEmpValid] *)
   try iSolveTC.
 
@@ -715,7 +747,7 @@ Local Ltac iSpecializeArgs_go H xs :=
   lazymatch xs with
   | hnil => idtac
   | hcons ?x ?xs =>
-     notypeclasses refine (tac_forall_specialize _ _ H _ _ _ _ _ _ _);
+     notypeclasses refine (tac_forall_specialize _ H _ _ _ _ _ _ _);
        [pm_reflexivity ||
         let H := pretty_ident H in
         fail "iSpecialize:" H "not found"
@@ -724,8 +756,8 @@ Local Ltac iSpecializeArgs_go H xs :=
         fail "iSpecialize: cannot instantiate" P "with" x
        |lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
         | |- ∃ _ : ?A, _ =>
-          notypeclasses refine (@ex_intro A _ x (conj _ _))
-        end; [shelve..|pm_reflexivity|iSpecializeArgs_go H xs]]
+          notypeclasses refine (@ex_intro A _ x _)
+        end; [shelve..|pm_reduce; iSpecializeArgs_go H xs]]
   end.
 Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
   iSpecializeArgs_go H xs.
@@ -791,7 +823,7 @@ Ltac iSpecializePat_go H1 pats :=
              fail "iSpecialize: cannot instantiate" P "with" Q
             |pm_reflexivity|iSpecializePat_go H1 pats]]
     | SPureGoal ?d :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -799,9 +831,9 @@ Ltac iSpecializePat_go H1 pats :=
          |iSolveTC ||
           let Q := match goal with |- FromPure _ ?Q _ => Q end in
           fail "iSpecialize:" Q "not pure"
-         |pm_reflexivity
          |solve_done d (*goal*)
-         |iSpecializePat_go H1 pats]
+         |pm_reduce;
+          iSpecializePat_go H1 pats]
     | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
        notypeclasses refine (tac_specialize_assert_intuitionistic _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
@@ -1063,22 +1095,22 @@ Tactic Notation "iRight" :=
      fail "iRight:" P "not a disjunction"
     |(* subgoal *)].
 
-Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
-  eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
+Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
+  eapply tac_or_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iOrDestruct:" H "not found"
     |iSolveTC ||
      let P := match goal with |- IntoOr ?P _ _ => P end in
      fail "iOrDestruct: cannot destruct" P
-    |pm_reflexivity ||
-     let H1 := pretty_ident H1 in
-     fail "iOrDestruct:" H1 "not fresh"
-    |pm_reflexivity ||
-     let H2 := pretty_ident H2 in
-     fail "iOrDestruct:" H2 "not fresh"
-    |(* subgoal 1 *)
-    |(* subgoal 2 *)].
+    | pm_reduce;
+      lazymatch goal with
+      | |- False =>
+        let H1 := pretty_ident H1 in
+        let H2 := pretty_ident H2 in
+        fail "iOrDestruct:" H1 "or" H2 "not fresh"
+      |  _ => split
+      end].
 
 (** * Conjunction and separating conjunction *)
 Tactic Notation "iSplit" :=
@@ -1094,35 +1126,39 @@ Tactic Notation "iSplitL" constr(Hs) :=
   iStartProof;
   let Hs := words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
-  eapply tac_sep_split with _ _ Left Hs _ _; (* (js:=Hs) *)
+  let Δ := iGetCtx in
+  eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
     [iSolveTC ||
      let P := match goal with |- FromSep _ ?P _ _ => P end in
      fail "iSplitL:" P "not a separating conjunction"
-    |pm_reflexivity ||
-     let Hs := iMissingHyps Hs in
-     fail "iSplitL: hypotheses" Hs "not found"
-    |(* subgoal 1 *)
-    |(* subgoal 2 *)].
+    |pm_reduce;
+     lazymatch goal with
+     | |- False => let Hs := iMissingHypsCore Δ Hs in
+                 fail "iSplitL: hypotheses" Hs "not found"
+     | _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
+     end].
 
 Tactic Notation "iSplitR" constr(Hs) :=
   iStartProof;
   let Hs := words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
-  eapply tac_sep_split with _ _ Right Hs _ _; (* (js:=Hs) *)
+  let Δ := iGetCtx in
+  eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *)
     [iSolveTC ||
      let P := match goal with |- FromSep _ ?P _ _ => P end in
      fail "iSplitR:" P "not a separating conjunction"
-    |pm_reflexivity ||
-     let Hs := iMissingHyps Hs in
-     fail "iSplitR: hypotheses" Hs "not found"
-    |(* subgoal 1 *)
-    |(* subgoal 2 *)].
+    |pm_reduce;
+     lazymatch goal with
+     | |- False => let Hs := iMissingHypsCore Δ Hs in
+                 fail "iSplitR: hypotheses" Hs "not found"
+     | _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
+     end].
 
 Tactic Notation "iSplitL" := iSplitR "".
 Tactic Notation "iSplitR" := iSplitL "".
 
 Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
-  eapply tac_and_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
+  eapply tac_and_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iAndDestruct:" H "not found"
@@ -1133,22 +1169,28 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
        | |- IntoAnd _ ?P _ _ => P
        end in
      fail "iAndDestruct: cannot destruct" P
-    |pm_reflexivity ||
-     let H1 := pretty_ident H1 in
-     let H2 := pretty_ident H2 in
-     fail "iAndDestruct:" H1 "or" H2 "not fresh"
-    |(* subgoal *)].
+    |pm_reduce;
+     lazymatch goal with
+       | |- False =>
+         let H1 := pretty_ident H1 in
+         let H2 := pretty_ident H2 in
+         fail "iAndDestruct:" H1 "or" H2 "not fresh"
+       | _ => idtac (* subgoal *)
+     end].
 
 Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
-  eapply tac_and_destruct_choice with _ H _ d H' _ _ _;
+  eapply tac_and_destruct_choice with H _ d H' _ _ _;
     [pm_reflexivity || fail "iAndDestructChoice:" H "not found"
     |pm_reduce; iSolveTC ||
      let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
      fail "iAndDestructChoice: cannot destruct" P
-    |pm_reflexivity ||
-     let H' := pretty_ident H' in
-     fail "iAndDestructChoice:" H' "not fresh"
-    |(* subgoal *)].
+    |pm_reduce;
+     lazymatch goal with
+     | |- False =>
+       let H' := pretty_ident H' in
+       fail "iAndDestructChoice:" H' "not fresh"
+     | _ => idtac (* subgoal *)
+     end].
 
 (** * Existential *)
 Tactic Notation "iExists" uconstr(x1) :=
@@ -1190,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) :=
@@ -1229,15 +1272,14 @@ Tactic Notation "iNext" := iModIntro (▷^_ _)%I.
 
 (** * Update modality *)
 Tactic Notation "iModCore" constr(H) :=
-  eapply tac_modal_elim with _ H _ _ _ _ _ _;
+  eapply tac_modal_elim with H _ _ _ _ _ _;
     [pm_reflexivity || fail "iMod:" H "not found"
     |iSolveTC ||
      let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in