From ded831d3199b7612546b0b128b1348fc63f6b576 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Fri, 24 May 2019 14:46:50 +0200
Subject: [PATCH] Fix error message regression, add new test cases.

Also fixes pre-existing bug in iCombine error messages.
---
 tests/proofmode.ref               |  61 ++++++-
 tests/proofmode.v                 |  56 ++++++-
 theories/proofmode/coq_tactics.v  | 265 ++++++++++++++++++++----------
 theories/proofmode/ltac_tactics.v | 261 +++++++++++++++++------------
 4 files changed, 443 insertions(+), 200 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index fb9e3a872..df2cc9712 100644
--- a/tests/proofmode.ref
+++ b/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:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7dfdf0f3d..07af70c40 100644
--- a/tests/proofmode.v
+++ b/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.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ea4b780b1..631e2f288 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -28,13 +28,17 @@ Lemma tac_eval Δ Q Q' :
   envs_entails Δ Q' → envs_entails Δ Q.
 Proof. by intros <-. Qed.
 
-Lemma tac_eval_in Δ Δ' i p P P' Q :
+Lemma tac_eval_in Δ i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   (∀ (P'':=P'), P ⊢ P') →
-  envs_simple_replace i p (Esnoc Enil i P') Δ  = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_simple_replace i p (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq /=. intros ? HP ? <-.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
+  rewrite envs_entails_eq /=. intros ? HP ?.
   rewrite envs_simple_replace_singleton_sound //; simpl.
   by rewrite HP wand_elim_r.
 Qed.
@@ -57,6 +61,7 @@ Proof. intros H. induction H; simpl; apply _. Qed.
 Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
 Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
 
+(* TODO: convert to not take Δ' *)
 Lemma tac_assumption Δ Δ' i p P Q :
   envs_lookup_delete true i Δ = Some (p,P,Δ') →
   FromAssumption p P Q →
@@ -70,16 +75,20 @@ Proof.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
-Lemma tac_rename Δ Δ' i j p P Q :
+Lemma tac_rename Δ i j p P Q :
   envs_lookup i Δ = Some (p,P) →
-  envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
-  envs_entails Δ' Q →
+  match envs_simple_replace i p (Esnoc Enil j P) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ?? <-. rewrite envs_simple_replace_singleton_sound //.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
+  rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
   by rewrite wand_elim_r.
 Qed.
 
+(* TODO: convert to not take Δ' *)
 Lemma tac_clear Δ Δ' i p P Q :
   envs_lookup_delete true i Δ = Some (p,P,Δ') →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
@@ -115,6 +124,7 @@ Proof.
   - by apply pure_intro.
 Qed.
 
+(* TODO: convert to not take Δ' *)
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete true i Δ = Some (p, P, Δ') →
   IntoPure P φ →
@@ -136,14 +146,18 @@ Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → env
 Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
 (** * Intuitionistic *)
-Lemma tac_intuitionistic Δ Δ' i p P P' Q :
+Lemma tac_intuitionistic Δ i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
-  envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_replace i p true (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=>?? HPQ ? HQ. rewrite envs_replace_singleton_sound //=.
+  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
+  rewrite envs_entails_eq=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
   destruct p; simpl; rewrite /bi_intuitionistically.
   - by rewrite -(into_persistent true P) /= wand_elim_r.
   - destruct HPQ.
@@ -155,14 +169,18 @@ Proof.
 Qed.
 
 (** * Implication and wand *)
-Lemma tac_impl_intro Δ Δ' i P P' Q R :
+Lemma tac_impl_intro Δ i P P' Q R :
   FromImpl R P Q →
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
-  envs_app false (Esnoc Enil i P') Δ = Some Δ' →
   FromAffinely P' P →
-  envs_entails Δ' Q → envs_entails Δ R.
+  match envs_app false (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromImpl envs_entails_eq => <- ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
+  destruct (envs_app _ _ _) eqn:?; last done.
+  rewrite /FromImpl envs_entails_eq => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
     rewrite -(from_affinely P' P) -affinely_and_lr.
@@ -170,13 +188,17 @@ Proof.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
     by rewrite -(from_affinely P' P) persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
-Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R :
+Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
   FromImpl R P Q →
   IntoPersistent false P P' →
-  envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ R.
+  match envs_app true (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromImpl envs_entails_eq => <- ?? <-.
+  destruct (envs_app _ _ _) eqn:?; last done.
+  rewrite /FromImpl envs_entails_eq => <- ??.
   rewrite envs_app_singleton_sound //=. apply impl_intro_l.
   rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
   by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
@@ -187,22 +209,31 @@ Proof.
   rewrite /FromImpl envs_entails_eq => <- ?. apply impl_intro_l. by rewrite and_elim_r.
 Qed.
 
-Lemma tac_wand_intro Δ Δ' i P Q R :
+Lemma tac_wand_intro Δ i P Q R :
   FromWand R P Q →
-  envs_app false (Esnoc Enil i P) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ R.
+  match envs_app false (Esnoc Enil i P) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromWand envs_entails_eq => <- ? HQ.
+  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
+  rewrite /FromWand envs_entails_eq => <- HQ.
   rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
-Lemma tac_wand_intro_intuitionistic Δ Δ' i P P' Q R :
+
+Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
   FromWand R P Q →
   IntoPersistent false P P' →
   TCOr (Affine P) (Absorbing Q) →
-  envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ R.
+  match envs_app true (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ R.
 Proof.
-  rewrite /FromWand envs_entails_eq => <- ? HPQ ? HQ.
+  destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
+  rewrite /FromWand envs_entails_eq => <- ? HPQ HQ.
   rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
             (into_persistent _ P) wand_elim_r //.
@@ -221,6 +252,7 @@ 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 Δ' or Δ'' *)
 Lemma tac_specialize remove_intuitionistic Δ Δ' Δ'' i p j q P1 P2 R Q :
   envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') →
   envs_lookup j Δ' = Some (q, R) →
@@ -276,14 +308,19 @@ Proof.
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert_pure Δ Δ' j q a R P1 P2 φ Q :
+Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand q true R P1 P2 →
   FromPure a P1 φ →
-  envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
-  φ → envs_entails Δ' Q → envs_entails Δ Q.
+  φ →
+  match envs_simple_replace j q (Esnoc Enil j P2) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ????? <-. rewrite envs_simple_replace_singleton_sound //=.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
+  rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
   rewrite -intuitionistically_if_idemp (into_wand q true) /=.
   rewrite -(from_pure a P1) pure_True //.
   rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
@@ -369,29 +406,45 @@ Proof.
   rewrite {1}intuitionistically_into_persistently_1 intuitionistically_elim impl_elim_r //.
 Qed.
 
-Lemma tac_assert Δ Δ' j P Q :
-  envs_app true (Esnoc Enil j (P -∗ P)%I) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+Lemma tac_assert Δ j P Q :
+  match envs_app true (Esnoc Enil j (P -∗ P)%I) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> ? <-. rewrite (envs_app_singleton_sound Δ) //; simpl.
+  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
+  rewrite envs_entails_eq=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
   by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
 Qed.
 
-Lemma tac_pose_proof Δ Δ' j P Q :
+Lemma tac_pose_proof Δ j P Q :
   P →
-  envs_app true (Esnoc Enil j P) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_app true (Esnoc Enil j P) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => HP ? <-. rewrite envs_app_singleton_sound //=.
+  destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
+  rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=.
   by rewrite -HP /= intuitionistically_emp emp_wand.
 Qed.
 
-Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
-  envs_lookup_delete false i Δ = Some (p, P, Δ') →
-  envs_app p (Esnoc Enil j P) Δ' = Some Δ'' →
-  envs_entails Δ'' Q → envs_entails Δ Q.
+Lemma tac_pose_proof_hyp Δ i j Q :
+  match envs_lookup_delete false i Δ with
+  | None => False
+  | Some (p, P, Δ') =>
+    match envs_app p (Esnoc Enil j P) Δ' with
+    | None => False
+    | Some Δ'' => envs_entails Δ'' Q
+    end
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ? <-.
+  destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
+  destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
+  rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *.
+  intros [? ->] <-.
   rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
   by rewrite wand_elim_r.
 Qed.
@@ -411,12 +464,15 @@ Lemma tac_and_split Δ P Q1 Q2 :
 Proof. rewrite envs_entails_eq. intros. rewrite -(from_and P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
-Lemma tac_sep_split Δ Δ1 Δ2 d js P Q1 Q2 :
+Lemma tac_sep_split Δ d js P Q1 Q2 :
   FromSep P Q1 Q2 →
-  envs_split d js Δ = Some (Δ1,Δ2) →
-  envs_entails Δ1 Q1 → envs_entails Δ2 Q2 → envs_entails Δ P.
+  match envs_split d js Δ with
+  | None => False
+  | Some (Δ1,Δ2) => envs_entails Δ1 Q1 ∧ envs_entails Δ2 Q2
+  end → envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq=>?? HQ1 HQ2.
+  destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
+  rewrite envs_entails_eq=>? [HQ1 HQ2].
   rewrite envs_split_sound //. by rewrite HQ1 HQ2.
 Qed.
 
@@ -446,12 +502,16 @@ Proof.
 Qed.
 
 (** * Conjunction/separating conjunction elimination *)
-Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
+Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) →
   (if p then IntoAnd true P P1 P2 else IntoSep P P1 P2) →
-  envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
   rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
   - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
   - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
@@ -460,16 +520,19 @@ Qed.
 (* Using this tactic, one can destruct a (non-separating) conjunction in the
 spatial context as long as one of the conjuncts is thrown away. It corresponds
 to the principle of "external choice" in linear logic. *)
-Lemma tac_and_destruct_choice Δ Δ' i p d j P P1 P2 Q :
+Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) →
   (if p then IntoAnd p P P1 P2 : Type else
     TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
       (if d is Left then TCOr (Affine P2) (Absorbing Q)
        else TCOr (Affine P1) (Absorbing Q)))) →
-  envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end → envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => ? HP ? HQ.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
+  rewrite envs_entails_eq => ? HP HQ.
   rewrite envs_simple_replace_singleton_sound //=. destruct p.
   { rewrite (into_and _ P) HQ. destruct d; simpl.
     - by rewrite and_elim_l wand_elim_r.
@@ -487,7 +550,7 @@ Qed.
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
   φ → Frame true ⌜φ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq => ?? ->. rewrite -(frame true ⌜φ⌝ P) /=.
+  rewrite envs_entails_eq => ? Hframe ->. rewrite -Hframe /=.
   rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
   auto using and_intro, pure_intro.
 Qed.
@@ -497,8 +560,8 @@ Lemma tac_frame Δ Δ' i p R P Q :
   Frame p R P Q →
   envs_entails Δ' Q → envs_entails Δ P.
 Proof.
-  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ? HQ.
-  rewrite (envs_lookup_sound' _ false) //. by rewrite -(frame p R P) HQ.
+  rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hframe HQ.
+  rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
 Qed.
 
 (** * Disjunction *)
@@ -513,13 +576,18 @@ Proof.
   rewrite envs_entails_eq=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
 Qed.
 
-Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
+Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoOr P P1 P2 →
-  envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
-  envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
-  envs_entails Δ1 Q → envs_entails Δ2 Q → envs_entails Δ Q.
+  match envs_simple_replace i p (Esnoc Enil j1 P1) Δ,
+        envs_simple_replace i p (Esnoc Enil j2 P2) Δ with
+  | Some Δ1, Some Δ2 => envs_entails Δ1 Q ∧ envs_entails Δ2 Q
+  | _, _ => False
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ???? HP1 HP2. rewrite envs_lookup_sound //.
+  destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; last done.
+  destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; last done.
+  rewrite envs_entails_eq. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
   rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
     by rewrite wand_elim_r.
@@ -534,14 +602,17 @@ Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q :
   envs_entails Δ Q.
 Proof. rewrite envs_entails_eq /FromForall=> <-. apply forall_intro. Qed.
 
-Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → PROP) Q :
+Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
   (∃ x : A,
-    envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' ∧
-    envs_entails Δ' Q) →
+      match envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ with
+      | None => False
+      | Some Δ' => envs_entails Δ' Q
+      end) →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq. intros ?? (x&?&?).
+  rewrite envs_entails_eq. intros ?? (x&?).
+  destruct (envs_simple_replace) as [Δ'|] eqn:?; last done.
   rewrite envs_simple_replace_singleton_sound //; simpl.
   by rewrite (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
@@ -560,26 +631,33 @@ 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.
 
 (** * Modalities *)
-Lemma tac_modal_elim Δ Δ' i p p' φ P' P Q Q' :
+Lemma tac_modal_elim Δ i p p' φ P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
   ElimModal φ p p' P P' Q Q' →
   φ →
-  envs_replace i p p' (Esnoc Enil i P') Δ = Some Δ' →
-  envs_entails Δ' Q' → envs_entails Δ Q.
+  match envs_replace i p p' (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q'
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => ???? HΔ. rewrite envs_replace_singleton_sound //=.
+  destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
+  rewrite envs_entails_eq => ??? HΔ. rewrite envs_replace_singleton_sound //=.
   rewrite HΔ. by eapply elim_modal.
 Qed.
 
@@ -598,18 +676,18 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
   envs_lookup_delete false i Δ = Some (p, Pinv, Δ') →
   ElimInv φ Pinv Pin Pout Pclose Q Q' →
   φ →
-  (∀ R, ∃ Δ'',
-    envs_app false (Esnoc Enil j
+  (∀ R,
+    match envs_app false (Esnoc Enil j
       (Pin -∗
        (∀ x, Pout x -∗ pm_option_fun Pclose x -∗? Q' x) -∗
        R
       )%I) Δ'
-      = Some Δ'' ∧
-    envs_entails Δ'' R) →
+    with Some Δ'' => envs_entails Δ'' R | None => False end) →
   envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) [Δ'' [? <-]].
-  rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
+  rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) Hmatch.
+  destruct (envs_app _ _ _) eqn:?; last done.
+  rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
   apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
   rewrite intuitionistically_if_elim -assoc. destruct Pclose; simpl in *.
   - setoid_rewrite wand_curry. auto.
@@ -864,15 +942,18 @@ Qed.
 Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
-  ∀ {A : ofeT} Δ' (x y : A) (Φ : A → PROP),
+  ∀ {A : ofeT} (x y : A) (Φ : A → PROP),
     IntoInternalEq Pxy x y →
     (P ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
-    envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
-    envs_entails Δ' Q →
+    match envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ with
+    | None => False
+    | Some Δ' => envs_entails Δ' Q
+    end →
     envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq /IntoInternalEq => ?? A Δ' x y Φ HPxy HP ?? <-.
+  rewrite envs_entails_eq /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
+  destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done. rewrite -Hentails.
   rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
   rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
   rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)%I) sep_elim_l.
@@ -913,12 +994,16 @@ Proof.
   - by rewrite Hs //= right_id.
 Qed.
 
-Lemma tac_löb Δ Δ' i Q :
+Lemma tac_löb Δ i Q :
   env_spatial_is_nil Δ = true →
-  envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
-  envs_entails Δ' Q → envs_entails Δ Q.
+  match envs_app true (Esnoc Enil i (▷ Q)%I) Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => ?? HQ.
+  destruct (envs_app _ _ _) eqn:?; last done.
+  rewrite envs_entails_eq => ? HQ.
   rewrite (env_spatial_is_nil_intuitionistically Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
   rewrite -(löb (<pers> Q)%I) later_persistently. apply impl_intro_l.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 94cac72a5..5685673f6 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/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
      let Q := match goal with |- ElimModal _ _ _ _ _ ?Q _ => Q end in
      fail "iMod: cannot eliminate modality" P "in" Q
     |iSolveSideCondition
-    |pm_reflexivity
-    |pm_prettify(* subgoal *)].
+    |pm_reduce; pm_prettify(* subgoal *)].
 
 (** * Basic destruct tactic *)
 Local Ltac iDestructHypGo Hz pat :=
@@ -1320,9 +1362,10 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
   let Hs := words Hs in
   let Hs := eval vm_compute in (INamed <$> Hs) in
   let H := iFresh in
+  let Δ := iGetCtx in
   eapply tac_combine with _ _ Hs _ _ H _;
     [pm_reflexivity ||
-     let Hs := iMissingHyps Hs in
+     let Hs := iMissingHypsCore Δ Hs in
      fail "iCombine: hypotheses" Hs "not found"
     |iSolveTC
     |pm_reflexivity ||
@@ -1990,11 +2033,15 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
   (* apply is sometimes confused wrt. canonical structures search.
      refine should use the other unification algorithm, which should
      not have this issue. *)
-  notypeclasses refine (tac_löb _ _ IH _ _ _ _);
+  notypeclasses refine (tac_löb _ IH _ _ _);
     [reflexivity || fail "iLöb: spatial context not empty, this should not happen"
-    |pm_reflexivity ||
-     let IH := pretty_ident IH in
-     fail "iLöb:" IH "not fresh"|].
+    |pm_reduce;
+     lazymatch goal with
+     | |- False =>
+       let IH := pretty_ident IH in
+       fail "iLöb:" IH "not fresh"
+     | _ => idtac
+     end].
 
 Tactic Notation "iLöbRevert" constr(Hs) "with" tactic(tac) :=
   iRevertIntros Hs with (
@@ -2065,9 +2112,9 @@ Tactic Notation "iAssertCore" open_constr(Q)
   | _ => fail "iAssert: exactly one specialization pattern should be given"
   end;
   let H := iFresh in
-  eapply tac_assert with _ H Q;
-    [pm_reflexivity
-    |iSpecializeCore H with hnil pats as p; [..|tac H]].
+  eapply tac_assert with H Q;
+  [pm_reduce;
+   iSpecializeCore H with hnil pats as p; [..|tac H]].
 
 Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
   let p := intro_pat_intuitionistic p in
@@ -2153,7 +2200,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity
-      |pm_reflexivity|pm_prettify; iClearHyp Heq]).
+      |pm_reduce; pm_prettify; iClearHyp Heq]).
 
 Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
   iRewriteCore Right lem in H.
@@ -2256,7 +2303,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
      let I := match goal with |- ElimInv _ ?I  _ _ _ _ _ => I end in
      fail "iInv: cannot eliminate invariant" I
     |iSolveSideCondition
-    |let R := fresh in intros R; eexists; split; [pm_reflexivity|];
+    |let R := fresh in intros R; pm_reduce;
      (* Now we are left proving [envs_entails Δ'' R]. *)
      iSpecializePat H pats; last (
        iApplyHyp H; clear R; pm_reduce;
-- 
GitLab