Skip to content
Snippets Groups Projects
Commit 12925885 authored by Ralf Jung's avatar Ralf Jung
Browse files

Fix coqdoc rendering 

fixes #437
parent bacc5968
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 2 deletions
iris/algebra/cmra.v
+ 3
− 2
View file @ 12925885
...@@ -1699,8 +1699,9 @@ Proof. ...@@ -1699,8 +1699,9 @@ Proof.
by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive. by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
Qed. Qed.
(** * Constructing a camera [B] through a bijection with [A] that (** * Constructing a camera [B] through a bijection with [A]
is mostly an isomorphism but restricts validity. *)
The bijection must be mostly an isomorphism but may restrict validity. *)
Lemma iso_cmra_mixin_restrict {A : cmra} {B : Type} Lemma iso_cmra_mixin_restrict {A : cmra} {B : Type}
`{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B} `{!Dist B, !Equiv B, !PCore B, !Op B, !Valid B, !ValidN B}
(f : A → B) (g : B → A) (f : A → B) (g : B → A)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment