Merge branch 'master-ofe_fun-doc' into 'master'

Fix documentation for ofe_funR See merge request iris/iris!236

Merge branch 'master-ofe_fun-doc' into 'master'
Fix documentation for ofe_funR See merge request iris/iris!236
195d3beb · Robbert Krebbers · 470c73cf · f25d9024 · 195d3beb
Commit 195d3beb authored Apr 29, 2019 by Robbert Krebbers
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1491,7 +1491,7 @@ Proof.
  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.

-(* Dependently-typed functions over a finite discrete domain *)
+(* Dependently-typed functions over a discrete domain *)
 Section ofe_fun_cmra.
  Context `{B : A → ucmraT}.
  Implicit Types f g : ofe_fun B.