Commit 995dc37b authored by Robbert's avatar Robbert

Merge branch 'fix-specialize-error-message' into 'master'

Fix error message when with [% //] fails

Closes #325

See merge request iris/iris!460
parents 11f9d567 1aec27cb
...@@ -94,6 +94,18 @@ The command has indeed failed with message: ...@@ -94,6 +94,18 @@ The command has indeed failed with message:
Tactic failure: iElaborateSelPat: "HQ" not found. Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message: The command has indeed failed with message:
Tactic failure: iElaborateSelPat: "HQ" not found. Tactic failure: iElaborateSelPat: "HQ" not found.
"test_iSpecialize_pure_error"
: string
The command has indeed failed with message:
Tactic failure: iSpecialize: P not pure.
"test_iSpecialize_pure_error"
: string
The command has indeed failed with message:
Tactic failure: iSpecialize: cannot solve φ using done.
"test_iSpecialize_done_error"
: string
The command has indeed failed with message:
Tactic failure: iSpecialize: cannot solve P using done.
The command has indeed failed with message: The command has indeed failed with message:
Tactic failure: iSpecialize: Q not persistent. Tactic failure: iSpecialize: Q not persistent.
"test_iAssert_intuitionistic" "test_iAssert_intuitionistic"
......
...@@ -184,6 +184,25 @@ Lemma test_iSpecialize_pure (φ : Prop) Q R : ...@@ -184,6 +184,25 @@ Lemma test_iSpecialize_pure (φ : Prop) Q R :
φ (⌜φ⌝ - Q) Q. φ (⌜φ⌝ - Q) Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed. Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iSpecialize_pure_done (φ: Prop) Q :
φ (⌜φ⌝ - Q) Q.
Proof. iIntros (HP) "HQ". iApply ("HQ" with "[% //]"). Qed.
Check "test_iSpecialize_pure_error".
Lemma test_iSpecialize_not_pure_error P Q :
(P - Q) Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[%]"). Abort.
Check "test_iSpecialize_pure_error".
Lemma test_iSpecialize_pure_done_error (φ: Prop) Q :
(⌜φ⌝ - Q) Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[% //]"). Abort.
Check "test_iSpecialize_done_error".
Lemma test_iSpecialize_done_error P Q :
(P - Q) Q.
Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[//]"). Abort.
Lemma test_iSpecialize_Coq_entailment P Q R : Lemma test_iSpecialize_Coq_entailment P Q R :
( P) (P - Q) ( Q). ( P) (P - Q) ( Q).
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed. Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
......
...@@ -845,9 +845,11 @@ Ltac iSpecializePat_go H1 pats := ...@@ -845,9 +845,11 @@ Ltac iSpecializePat_go H1 pats :=
let solve_done d := let solve_done d :=
lazymatch d with lazymatch d with
| true => | true =>
done || first [ done
let Q := match goal with |- envs_entails _ ?Q => Q end in | let Q := match goal with |- envs_entails _ ?Q => Q end in
fail "iSpecialize: cannot solve" Q "using done" fail 1 "iSpecialize: cannot solve" Q "using done"
| let Q := match goal with |- ?Q => Q end in
fail 1 "iSpecialize: cannot solve" Q "using done" ]
| false => idtac | false => idtac
end in end in
let Δ := iGetCtx in let Δ := iGetCtx in
......
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