From f25d9024cf60f4c70d479f79d150ea9feb5afc62 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 29 Apr 2019 03:23:25 +0200
Subject: [PATCH] Fix documentation for ofe_funR

This comment wasn't updated after
866cad626abd0c827d61f4921290b5e5abe630a1.
---
 theories/algebra/cmra.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d4418c515..44d2d1774 100644
--- 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.
-- 
GitLab