From d5d4ebf30ec5c48457bff34e603ad01413851ca4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 29 Aug 2020 14:06:49 +0200
Subject: [PATCH] adjust proofmode comment

---
 theories/proofmode/environments.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index a9e797c0c..1be6f6992 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -237,9 +237,9 @@ way, [iFresh] can simply be implemented by changing the goal from
 using the tactic [convert_concl_no_check]. This way, the generated proof term
 contains no additional steps for changing the counter.
 
-For all definitions below, we first define a version that take the two contexts
-[env_intuitionistic] and [env_spatial] as its arguments, and then lift these
-definitions that take the whole proof mode context [Δ : envs PROP]. This is
+We first define a version [pre_envs_entails] that takes the two contexts
+[env_intuitionistic] and [env_spatial] as its arguments. We seal this definition
+and then lift it to take the whole proof mode context [Δ : envs PROP]. This is
 crucial to make sure that the counter [env_counter] is not part of the seal. *)
 Record envs_wf' {PROP : bi} (Γp Γs : env PROP) := {
   env_intuitionistic_valid : env_wf Γp;
-- 
GitLab