From 730f24ecd0755859346e0e8df8adbac2eb99b935 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Mar 2021 19:34:13 +0100
Subject: [PATCH] slightly extend iPureIntro automation comment

---
 iris/proofmode/ltac_tactics.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 9aa8bc766..ad529cf61 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3325,7 +3325,9 @@ Tactic Notation "iAccu" :=
 Global Hint Extern 0 (_ ⊢ _) => iStartProof : core.
 Global Hint Extern 0 (⊢ _) => iStartProof : core.
 
-(* Make sure that by and done solve trivial things in proof mode *)
+(* Make sure that [by] and [done] solve trivial things in proof mode.
+[iPureIntro] invokes [FromPure], so adding [FromPure] instances can help improve
+what [done] can do. *)
 Global Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
 Global Hint Extern 0 (envs_entails _ ?Q) =>
   first [is_evar Q; fail 1|iAssumption] : core.
-- 
GitLab