diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 86b3c0c97e2e4d16de541fa879781a5c02798956..9df5355cdbeb3e6c4b00ef2fa4a87edc34bf9fe7 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.