diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d35386930c066efdd93f16d620dc4efc5c47aa95..27fc8f8d4e1cf29c17997ec7f2ada3716edc99f0 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.