From cbb493e77ae05d36a96a975f7b98399134910d98 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 7 Dec 2017 11:12:04 +0100
Subject: [PATCH] Remove useless comment.

---
 theories/base_logic/upred.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 82abe8a6d..ee3899838 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -9,9 +9,6 @@ Set Default Proof Using "Type".
 Record uPred (M : ucmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
 
-  (* [uPred_mono] is used to prove non-expansiveness (guaranteed by
-     [uPred_ne]). Therefore, it is important that we do not restrict
-     it to only valid elements. *)
   uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
 
   uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → uPred_holds n2 x
-- 
GitLab