From fa0e8eb87bea55c29f165e2a4d4a9d3de947e946 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Apr 2018 23:48:55 +0200
Subject: [PATCH] Let `done` and friends fail when the proofmode goal is an
 evar.

This fixes issue #182.
---
 theories/proofmode/tactics.v | 3 ++-
 theories/tests/proofmode.v   | 5 ++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 87fe3ef65..b9592351d 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -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
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index e8d30aa73..a79341f8a 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -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.
-- 
GitLab