Merge branch 'joe/fix_iSpecialize_regression' into 'master'

Fix regression with iSpecialize errors.

See merge request iris/iris!262

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:

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.

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 _ _);