when the goal is an evar, pick emp when possible

Fixes #182

theories/proofmode/tactics.v

@@ -1964,8 +1964,7 @@ 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 _ emp) => iEmpIntro.
+Hint Extern 0 (envs_entails _ _) => iEmpIntro || iAssumption.
 
 (* TODO: look for a more principled way of adding trivial hints like those
 below; see the discussion in !75 for further details. *)

theories/tests/proofmode.v

@@ -112,7 +112,7 @@ Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
   P -∗ Q → R -∗ emp.
 Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
 
-Let test_fresh P Q:
+Lemma test_fresh P Q:
   (P ∗ Q) -∗ (P ∗ Q).
 Proof.
   iIntros "H".
@@ -428,7 +428,19 @@ Proof.
 Qed.
 
 Lemma test_iAssumption_False_no_loop : ∃ R, R ⊢ ∀ P, P.
-Proof. eexists. iIntros "?" (P). done. Qed.
+Proof.
+  eexists. iIntros "?" (P).
+  (* Can't pick P as R must not depend on P. *)
+  done.
+Qed.
+
+Lemma test_goal_evar P : ∃ R, (□ P ⊢ R) ∧ R = emp%I.
+Proof.
+  eexists. split.
+  - iIntros "#HP". done.
+  (* Now verify that we picked emp, and not □ P. *)
+  - reflexivity.
+Qed.
 
 Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
   P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).