From 15b4a65e5365c83f65ee5f090f3b17d616bf7495 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 19 Apr 2018 16:22:42 +0200
Subject: [PATCH] when the goal is an evar, pick emp when possible

Fixes #182
---
 theories/proofmode/tactics.v |  3 +--
 theories/tests/proofmode.v   | 16 ++++++++++++++--
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 87fe3ef65..5463b3ead 100644
--- a/theories/proofmode/tactics.v
+++ b/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. *)
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index e8d30aa73..b00037edd 100644
--- a/theories/tests/proofmode.v
+++ b/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).
-- 
GitLab