From 129258855b41e46a41141feff79b5833d9eb67b8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 19 Oct 2021 11:57:22 -0400
Subject: [PATCH] Fix coqdoc rendering

fixes #437
---
 iris/algebra/cmra.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index c8424ccff..c9b1a2f94 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1699,8 +1699,9 @@ Proof.
   by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
 Qed.
 
-(** * Constructing a camera [B] through a bijection with [A] that
-is mostly an isomorphism but restricts validity. *)
+(** * Constructing a camera [B] through a bijection with [A]
+
+The bijection must be mostly an isomorphism but may restrict validity. *)
 Lemma iso_cmra_mixin_restrict {A : cmra} {B : Type}
   `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
   (f : A → B) (g : B → A)
-- 
GitLab