diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 7059e8b611b07ae64456d268df9b4162b19a2c60..ed6254f0bee39fef95c92d7abce8d3738bc08965 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -765,7 +765,7 @@ Section cmra_morphism.
 End cmra_morphism.
 
 (** Functors *)
-Structure rFunctor := RFunctor {
+Record rFunctor := RFunctor {
   rFunctor_car : ofeT → ofeT → cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
@@ -798,7 +798,7 @@ Coercion constRF : cmraT >-> rFunctor.
 Instance constRF_contractive B : rFunctorContractive (constRF B).
 Proof. rewrite /rFunctorContractive; apply _. Qed.
 
-Structure urFunctor := URFunctor {
+Record urFunctor := URFunctor {
   urFunctor_car : ofeT → ofeT → ucmraT;
   urFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index f7672c263c6b1ec6c4c3eebe8b642ff2260d01a5..6db8d6e8054f453cc9a078f86ddb4b72e3998485 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -663,7 +663,7 @@ Instance prodC_map_ne {A A' B B'} :
 Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
 (** Functors *)
-Structure cFunctor := CFunctor {
+Record cFunctor := CFunctor {
   cFunctor_car : ofeT → ofeT → ofeT;
   cFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;