Commit be28173f authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix error handling of iPoseProofCoreHyp.

parent 2d209fea
......@@ -559,6 +559,23 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"<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:
......
......@@ -839,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.
......
......@@ -707,20 +707,21 @@ Local Ltac iIntoEmpValid t :=
|exact t]].
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
let Δ := iGetCtx in
eapply tac_pose_proof_hyp with H Hnew;
pm_reduce;
lazymatch goal with
| |- False =>
let H := pretty_ident H in
fail "iPoseProof:" H "not found"
| _ =>
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"
| _ => idtac
end
| _ => idtac
end.
Tactic Notation "iPoseProofCoreLem"
......
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