From 51125453bf84182a6c0aa594096798ef1e756b23 Mon Sep 17 00:00:00 2001
From: Robbert <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 14 Sep 2020 20:31:43 +0200
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)

---
 theories/algebra/cmra.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index e7b930a27..cb92fba97 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1669,7 +1669,8 @@ Proof.
   by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
 Qed.
 
-(** * Constructing a camera by restricting validity *)
+(** * Constructing a camera [B] through a bijection with [A] that
+is mostly an isomorphism but restricts validity. *)
 Lemma iso_cmra_mixin_restrict {A : cmraT} {B : Type}
   `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
   (f : A → B) (g : B → A)
-- 
GitLab