Commit 6a468eca authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Fix regression with iSpecialize errors.

parent b7c688d0
...@@ -576,6 +576,26 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)", ...@@ -576,6 +576,26 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and "iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
"iPoseProofCoreHyp (constr) as (constr)", last call failed. "iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found. 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" "iPoseProofCoreHyp_not_found_fail"
: string : string
The command has indeed failed with message: The command has indeed failed with message:
......
...@@ -859,6 +859,12 @@ Proof. ...@@ -859,6 +859,12 @@ Proof.
iIntros "H". Fail iPoseProof "Hx" as "H1". iIntros "H". Fail iPoseProof "Hx" as "H1".
Abort. 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". Check "iPoseProofCoreHyp_not_found_fail".
Lemma iPoseProofCoreHyp_not_found_fail P : P - P - P. Lemma iPoseProofCoreHyp_not_found_fail P : P - P - P.
Proof. Proof.
......
...@@ -777,6 +777,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -777,6 +777,7 @@ Ltac iSpecializePat_go H1 pats :=
fail "iSpecialize: cannot solve" Q "using done" fail "iSpecialize: cannot solve" Q "using done"
| false => idtac | false => idtac
end in end in
let Δ := iGetCtx in
lazymatch pats with lazymatch pats with
| [] => idtac | [] => idtac
| SForall :: ?pats => | SForall :: ?pats =>
...@@ -864,7 +865,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -864,7 +865,7 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reduce; |pm_reduce;
lazymatch goal with lazymatch goal with
| |- False => | |- False =>
let Hs' := iMissingHyps Hs' in let Hs' := iMissingHypsCore Δ Hs' in
fail "iSpecialize: hypotheses" Hs' "not found" fail "iSpecialize: hypotheses" Hs' "not found"
| _ => | _ =>
notypeclasses refine (conj _ _); notypeclasses refine (conj _ _);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment