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

This fixes issue #182.

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

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.