From 6a468eca77a9ab9df3bf4ad4f9d634c24a4288f3 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Sun, 9 Jun 2019 16:02:41 -0400
Subject: [PATCH] Fix regression with iSpecialize errors.

---
 tests/proofmode.ref               | 20 ++++++++++++++++++++
 tests/proofmode.v                 |  6 ++++++
 theories/proofmode/ltac_tactics.v |  3 ++-
 3 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index c04c2b4a9..e1ab0ee88 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -576,6 +576,26 @@ 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.
+"iPoseProof_not_found_fail2"
+     : 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)",
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
+"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
+"spec_tac" (bound to
+fun _ =>
+  lazymatch lem with
+  | {| itrm := _; itrm_vars := ?xs; itrm_hyps := ?pat |} => iSpecializeCore
+  {| itrm := Htmp; itrm_vars := xs; itrm_hyps := pat |} as p
+  | _ => idtac
+  end), "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: hypotheses ["HQ"] not found.
 "iPoseProofCoreHyp_not_found_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 54f4663b5..515cb9dbd 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -859,6 +859,12 @@ Proof.
   iIntros "H". Fail iPoseProof "Hx" as "H1".
 Abort.
 
+Check "iPoseProof_not_found_fail2".
+Lemma iPoseProof_not_found_fail2 P Q (H: P -∗ Q) : P -∗ Q.
+Proof.
+  iIntros "HP". Fail iPoseProof (H with "[HQ]") as "H".
+Abort.
+
 Check "iPoseProofCoreHyp_not_found_fail".
 Lemma iPoseProofCoreHyp_not_found_fail P : P -∗ P -∗ P.
 Proof.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index b8fd46530..dff46653b 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -777,6 +777,7 @@ Ltac iSpecializePat_go H1 pats :=
        fail "iSpecialize: cannot solve" Q "using done"
     | false => idtac
     end in
+  let Δ := iGetCtx in
   lazymatch pats with
     | [] => idtac
     | SForall :: ?pats =>
@@ -864,7 +865,7 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reduce;
           lazymatch goal with
           | |- False =>
-            let Hs' := iMissingHyps Hs' in
+            let Hs' := iMissingHypsCore Δ Hs' in
             fail "iSpecialize: hypotheses" Hs' "not found"
           | _ =>
             notypeclasses refine (conj _ _);
-- 
GitLab