diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 381e2e9fef5cad9d4a7da658eea0d3d860a2b326..d35386930c066efdd93f16d620dc4efc5c47aa95 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 *)
+(* Dependently-typed functions over a finite domain *)
 Section ofe_fun_cmra.
   Context `{Hfin : Finite A} {B : A → ucmraT}.
   Implicit Types f g : ofe_fun B.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c5e8e4042571cf642d0bd379d6659bb44c5ab4d2..eb422ac9b8a73bb933c48f2cfa10cd34bd47bc6a 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1087,7 +1087,7 @@ Proof.
   destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
-(* Dependently-typed functions *)
+(* Dependently-typed functions over a discrete domain *)
 (* We make [ofe_fun] a definition so that we can register it as a canonical
 structure. *)
 Definition ofe_fun {A} (B : A → ofeT) := ∀ x : A, B x.