Commit 46cc91ed authored by Ralf Jung's avatar Ralf Jung

Merge branch 'robbert/done_evar' into 'gen_proofmode'

Let `done` and friends fail when the proofmode goal is an evar.

See merge request FP/iris-coq!140
parents 840ce3af fa0e8eb8
......@@ -1964,7 +1964,8 @@ Hint Extern 0 (_ ⊢ _) => iStartProof.
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (envs_entails _ _) => iPureIntro; try done.
Hint Extern 0 (envs_entails _ _) => iAssumption.
Hint Extern 0 (envs_entails _ ?Q) =>
first [is_evar Q; fail 1|iAssumption].
Hint Extern 0 (envs_entails _ emp) => iEmpIntro.
(* TODO: look for a more principled way of adding trivial hints like those
......
......@@ -86,6 +86,9 @@ Proof. eexists. iIntros "?" (P). iAssumption. Qed.
Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P - Q - R - Q.
Proof. iIntros "H1 H2 H3". iAssumption. Qed.
Lemma test_done_goal_evar Q : P, Q P.
Proof. eexists. iIntros "H". Fail done. iAssumption. Qed.
Lemma test_iDestruct_spatial_and P Q1 Q2 : P (Q1 Q2) - P Q1.
Proof. iIntros "[H [? _]]". by iFrame. Qed.
......@@ -405,7 +408,7 @@ Lemma iFrame_with_evar_l P Q :
R, (P - Q - R P) R = Q.
Proof.
eexists. split. iIntros "HP HQ". Fail iFrame "HQ".
by iSplitR "HP". done.
iSplitR "HP"; iAssumption. done.
Qed.
Lemma iFrame_with_evar_persistent P Q :
R, (P - Q - P R Q) R = emp%I.
......
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