From df8491435496b8f68bd60a1e2c2de4cf9cccde0f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Mar 2019 19:37:22 +0100
Subject: [PATCH] move comment into appropriate section

---
 theories/base_logic/bi.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index dd7f9f7e5..72c3ea3e3 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -211,9 +211,9 @@ Proof. apply pure_soundness. Qed.
 
 Lemma later_soundness P : bi_emp_valid (▷ P) → bi_emp_valid P.
 Proof. apply later_soundness. Qed.
+(** See [derived.v] for a similar soundness result for basic updates. *)
 End restate.
 
-(** See [derived.v] for the version for basic updates. *)
 
 (** New unseal tactic that also unfolds the BI layer.
     This is used by [base_logic.double_negation].
-- 
GitLab