diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index c04c2b4a9e5d125424f0df847c5429a492674d21..e1ab0ee889e8ae99abeb59db2dad4ae123432db7 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 54f4663b516486ca15b44d4586c2efe183fb516e..515cb9dbd80f741b8193195789d066dd882a0a8e 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 b8fd465302fe6cb3f642ca3bc4fdf68df6be9f86..dff46653bee6b1936ba82cf24161028370356167 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 _ _);