Skip to content
Snippets Groups Projects
Commit 2ed3de6b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix some comments.

parent cec05125
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/algebra/cmra.v
+ 1
− 1
View file @ 2ed3de6b
...@@ -1464,7 +1464,7 @@ Proof. ...@@ -1464,7 +1464,7 @@ Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive. by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed. Qed.
(* Dependently-typed functions *) (* Dependently-typed functions over a finite domain *)
Section ofe_fun_cmra. Section ofe_fun_cmra.
Context `{Hfin : Finite A} {B : A → ucmraT}. Context `{Hfin : Finite A} {B : A → ucmraT}.
Implicit Types f g : ofe_fun B. Implicit Types f g : ofe_fun B.
......
theories/algebra/ofe.v
+ 1
− 1
View file @ 2ed3de6b
...@@ -1087,7 +1087,7 @@ Proof. ...@@ -1087,7 +1087,7 @@ Proof.
destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg. destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
Qed. Qed.
(* Dependently-typed functions *) (* Dependently-typed functions over a discrete domain *)
(* We make [ofe_fun] a definition so that we can register it as a canonical (* We make [ofe_fun] a definition so that we can register it as a canonical
structure. *) structure. *)
Definition ofe_fun {A} (B : A → ofeT) := ∀ x : A, B x. Definition ofe_fun {A} (B : A → ofeT) := ∀ x : A, B x.
......
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