diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 1cd3f8d222b52321c57c4577dd64b736e09ae4cd..f2ed6b23cd30d5d0c3a79abd8e086f57c1c68534 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -774,7 +774,7 @@ Section cmra_morphism.
   Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.
 End cmra_morphism.
 
-(** OFE → CMRA Functors *)
+(** COFE → CMRA Functors *)
 Record rFunctor := RFunctor {
   rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmraT;
   rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
@@ -812,7 +812,7 @@ Coercion constRF : cmraT >-> rFunctor.
 Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
-(** OFE → UCMRA Functors *)
+(** COFE → UCMRA Functors *)
 Record urFunctor := URFunctor {
   urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmraT;
   urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index d9a817ce96c719512a1be7deb2388ede5cf57834..4eae60614245cb06c1c17ddc3318b74949a2c988 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -684,7 +684,7 @@ Instance prodO_map_ne {A A' B B'} :
   NonExpansive2 (@prodO_map A A' B B').
 Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
-(** OFE → OFE Functors *)
+(** COFE → OFE Functors *)
 Record oFunctor := OFunctor {
   oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
   oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :