From 7479b01bb2714b45cb761867e57edca051096bba Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Feb 2018 18:35:40 +0100
Subject: [PATCH] Add comment.

---
 theories/proofmode/coq_tactics.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9e971ae75..86966e8c5 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -524,6 +524,8 @@ Proof.
 Qed.
 
 (** * Pure *)
+(* This relies on the invariant that [FromPure false] implies
+   [FromPure true] *)
 Lemma tac_pure_intro Δ Q φ af :
   env_spatial_is_nil Δ = af → FromPure af Q φ → φ → envs_entails Δ Q.
 Proof.
-- 
GitLab