From 606a252ed9751c05543b35b974bc5e73b178057a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 28 Nov 2017 10:31:13 +0100
Subject: [PATCH] more precise comment

---
 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 d35386930..27fc8f8d4 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1464,7 +1464,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 domain *)
+(* Dependently-typed functions over a finite discrete domain *)
 Section ofe_fun_cmra.
   Context `{Hfin : Finite A} {B : A → ucmraT}.
   Implicit Types f g : ofe_fun B.
-- 
GitLab