diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d4418c515e2d989ff513ce006dfa32448a8228e1..44d2d177421f95325a5033b0a57e4e4b9660d04f 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.