diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index ee4d65d20b86764decf7d0de98e076abb687fec6..1071f99732248863931bdd804bcd2f429aaf2580 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -310,20 +310,20 @@ Program Definition agreeRF (F : oFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := agreeO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_ne.
+  intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl. by apply agreeO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(agree_map_id x).
-  apply (agree_map_ext _)=>y. by rewrite oFunctor_id.
+  apply (agree_map_ext _)=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -agree_map_compose.
-  apply (agree_map_ext _)=>y; apply oFunctor_compose.
+  apply (agree_map_ext _)=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance agreeRF_contractive F :
   oFunctorContractive F → rFunctorContractive (agreeRF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ???; simpl.
-  by apply agreeO_map_ne, oFunctor_contractive.
+  by apply agreeO_map_ne, oFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 90441e3150f2ad191addc3b020075f66059e8427..49467a7703537cae0736836e341a18c01566f53c 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -455,21 +455,21 @@ Program Definition authRF (F : urFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
-  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
-  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance authRF_contractive F :
   urFunctorContractive F → rFunctorContractive (authRF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
 Qed.
 
 Program Definition authURF (F : urFunctor) : urFunctor := {|
@@ -477,19 +477,19 @@ Program Definition authURF (F : urFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := authO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(auth_map_id x).
-  apply (auth_map_ext _ _)=>y; apply urFunctor_id.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -auth_map_compose.
-  apply (auth_map_ext _ _)=>y; apply urFunctor_compose.
+  apply (auth_map_ext _ _)=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance authURF_contractive F :
   urFunctorContractive F → urFunctorContractive (authURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply authO_map_ne, urFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b0f608cc58b6b1617f985a785ab302e26386ae88..505f56807423e9d0dbec92f65c200f2d9c25fe98 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -779,25 +779,25 @@ Record rFunctor := RFunctor {
   rFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, cmraT;
   rFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+  rFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     NonExpansive (@rFunctor_map A1 _ A2 _ B1 _ B2 _);
-  rFunctor_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
+  rFunctor_map_id `{!Cofe A, !Cofe B} (x : rFunctor_car A B) :
     rFunctor_map (cid,cid) x ≡ x;
-  rFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
+  rFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     rFunctor_map (f◎g, g'◎f') x ≡ rFunctor_map (g,g') (rFunctor_map (f,f') x);
   rFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
       (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (rFunctor_map fg)
 }.
-Existing Instances rFunctor_ne rFunctor_mor.
+Existing Instances rFunctor_map_ne rFunctor_mor.
 Instance: Params (@rFunctor_map) 9 := {}.
 
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
 
 Class rFunctorContractive (F : rFunctor) :=
-  rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  rFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
 Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
@@ -816,25 +816,25 @@ Record urFunctor := URFunctor {
   urFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ucmraT;
   urFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
-  urFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+  urFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     NonExpansive (@urFunctor_map A1 _ A2 _ B1 _ B2 _);
-  urFunctor_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
+  urFunctor_map_id `{!Cofe A, !Cofe B} (x : urFunctor_car A B) :
     urFunctor_map (cid,cid) x ≡ x;
-  urFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
+  urFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     urFunctor_map (f◎g, g'◎f') x ≡ urFunctor_map (g,g') (urFunctor_map (f,f') x);
   urFunctor_mor `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2}
       (fg : (A2 -n> A1) * (B1 -n> B2)) :
     CmraMorphism (urFunctor_map fg)
 }.
-Existing Instances urFunctor_ne urFunctor_mor.
+Existing Instances urFunctor_map_ne urFunctor_mor.
 Instance: Params (@urFunctor_map) 9 := {}.
 
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
 
 Class urFunctorContractive (F : urFunctor) :=
-  urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  urFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
 Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
@@ -1253,12 +1253,12 @@ Program Definition prodRF (F1 F2 : rFunctor) : rFunctor := {|
     prodO_map (rFunctor_map F1 fg) (rFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply rFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !rFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
-  by rewrite !rFunctor_compose.
+  by rewrite !rFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.
 
@@ -1267,7 +1267,7 @@ Instance prodRF_contractive F1 F2 :
   rFunctorContractive (prodRF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply prodO_map_ne; apply rFunctor_contractive.
+    by apply prodO_map_ne; apply rFunctor_map_contractive.
 Qed.
 
 Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
@@ -1276,12 +1276,12 @@ Program Definition prodURF (F1 F2 : urFunctor) : urFunctor := {|
     prodO_map (urFunctor_map F1 fg) (urFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_ne.
+  intros F1 F2 A1 ? A2 ? B1 ? B2 ? n ???. by apply prodO_map_ne; apply urFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !urFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
-  by rewrite !urFunctor_compose.
+  by rewrite !urFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodURF F1%URF F2%URF) : urFunctor_scope.
 
@@ -1290,7 +1290,7 @@ Instance prodURF_contractive F1 F2 :
   urFunctorContractive (prodURF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply prodO_map_ne; apply urFunctor_contractive.
+    by apply prodO_map_ne; apply urFunctor_map_contractive.
 Qed.
 
 (** ** CMRA for the option type *)
@@ -1527,21 +1527,21 @@ Program Definition optionRF (F : rFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
 Qed.
 
 Instance optionRF_contractive F :
   rFunctorContractive F → rFunctorContractive (optionRF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
 Program Definition optionURF (F : rFunctor) : urFunctor := {|
@@ -1549,21 +1549,21 @@ Program Definition optionURF (F : rFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_map_compose.
 Qed.
 
 Instance optionURF_contractive F :
   rFunctorContractive F → urFunctorContractive (optionURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, rFunctor_map_contractive.
 Qed.
 
 (* Dependently-typed functions over a discrete domain *)
@@ -1650,19 +1650,19 @@ Program Definition discrete_funURF {C} (F : C → urFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, urFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_ne.
+  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
-  apply discrete_fun_map_ext=> y; apply urFunctor_id.
+  apply discrete_fun_map_ext=> y; apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g. rewrite /=-discrete_fun_map_compose.
-  apply discrete_fun_map_ext=>y; apply urFunctor_compose.
+  apply discrete_fun_map_ext=>y; apply urFunctor_map_compose.
 Qed.
 Instance discrete_funURF_contractive {C} (F : C → urFunctor) :
   (∀ c, urFunctorContractive (F c)) → urFunctorContractive (discrete_funURF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
-  by apply discrete_funO_map_ne=>c; apply urFunctor_contractive.
+  by apply discrete_funO_map_ne=>c; apply urFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index f64b166540f9ff2986746d2599e09e1f51351546..f5a1900511bf1f0f1070cd9fa319f9ef1e9064a9 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -34,14 +34,15 @@ Arguments g : simpl never.
 Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
 Proof using Fcontr.
   induction k as [|k IH]; simpl in *; [by destruct x|].
-  rewrite -oFunctor_compose -{2}[x]oFunctor_id. by apply (contractive_proper map).
+  rewrite -oFunctor_map_compose -{2}[x]oFunctor_map_id.
+  by apply (contractive_proper map).
 Qed.
 Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
 Proof using Fcontr.
   induction k as [|k IH]; simpl.
-  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
+  - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
     apply (contractive_0 map).
-  - rewrite f_S g_S -{2}[x]oFunctor_id -oFunctor_compose.
+  - rewrite f_S g_S -{2}[x]oFunctor_map_id -oFunctor_map_compose.
     by apply (contractive_S map).
 Qed.
 
@@ -183,7 +184,7 @@ Next Obligation.
   assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
   induction k as [|k IH]; simpl; first done.
   rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
-  rewrite f_S -oFunctor_compose.
+  rewrite f_S -oFunctor_map_compose.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
 Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X).
@@ -197,7 +198,7 @@ Program Definition fold (X : oFunctor_apply F T) : T :=
   {| tower_car n := g n (map (embed' n,project n) X) |}.
 Next Obligation.
   intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
-  rewrite g_S -oFunctor_compose.
+  rewrite g_S -oFunctor_map_compose.
   apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
 Qed.
 Instance fold_ne : NonExpansive fold.
@@ -212,7 +213,7 @@ Proof using Type*.
     { rewrite /unfold (conv_compl n (unfold_chain X)).
       rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
       rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
-      rewrite f_S -!oFunctor_compose; apply (contractive_ne map); split=> Y.
+      rewrite f_S -!oFunctor_map_compose; apply (contractive_ne map); split=> Y.
       + rewrite /embed' /= /embed_coerce.
         destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
         by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
@@ -222,14 +223,14 @@ Proof using Type*.
     assert (∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
       map (ff i, gg i) x ≡ gg i (coerce H x)) as map_ff_gg.
     { intros i; induction i as [|i IH]; intros k' x H; simpl.
-      { by rewrite coerce_id oFunctor_id. }
-      rewrite oFunctor_compose g_coerce; apply IH. }
+      { by rewrite coerce_id oFunctor_map_id. }
+      rewrite oFunctor_map_compose g_coerce; apply IH. }
     assert (H: S n + k = n + S k) by lia.
     rewrite (map_ff_gg _ _ _ H).
     apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
   - intros X; rewrite equiv_dist=> n /=.
     rewrite /unfold /= (conv_compl' n (unfold_chain (fold X))) /=.
-    rewrite g_S -!oFunctor_compose -{2}[X]oFunctor_id.
+    rewrite g_S -!oFunctor_map_compose -{2}[X]oFunctor_map_id.
     apply (contractive_ne map); split => Y /=.
     + rewrite f_tower. apply dist_S. by rewrite embed_tower.
     + etrans; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 86d121530b3324068869965191cdac31736212d8..477c3f3e51efd780b7ef49b87d6ab729b860a1cd 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -375,15 +375,15 @@ Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
 |}.
 Next Obligation.
-  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumO_map_ne; try apply rFunctor_ne.
+  by intros Fa Fb A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply csumO_map_ne; try apply rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros Fa Fb A ? B ? x. rewrite /= -{2}(csum_map_id x).
-  apply csum_map_ext=>y; apply rFunctor_id.
+  apply csum_map_ext=>y; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros Fa Fb A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -csum_map_compose.
-  apply csum_map_ext=>y; apply rFunctor_compose.
+  apply csum_map_ext=>y; apply rFunctor_map_compose.
 Qed.
 
 Instance csumRF_contractive Fa Fb :
@@ -391,5 +391,5 @@ Instance csumRF_contractive Fa Fb :
   rFunctorContractive (csumRF Fa Fb).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg.
-  by apply csumO_map_ne; try apply rFunctor_contractive.
+  by apply csumO_map_ne; try apply rFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 6467624323e8915259dde9528e4a56be58ad5d90..027517d48d8cf92a6de77a4c98540e729ee89d57 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -154,19 +154,19 @@ Program Definition exclRF (F : oFunctor) : rFunctor := {|
   rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := exclO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_ne.
+  intros F A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(excl_map_id x).
-  apply excl_map_ext=>y. by rewrite oFunctor_id.
+  apply excl_map_ext=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -excl_map_compose.
-  apply excl_map_ext=>y; apply oFunctor_compose.
+  apply excl_map_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance exclRF_contractive F :
   oFunctorContractive F → rFunctorContractive (exclRF F).
 Proof.
-  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_contractive.
+  intros A1 ? A2 ? B1 ? B2 ? n x1 x2 ??. by apply exclO_map_ne, oFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index d499dfa7db0c15fe543000009094b351e4ecf2fb..01d97b757819dc562af34bee7ca915f02aa0e4e2 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -628,20 +628,20 @@ Program Definition gmapOF K `{Countable K} (F : oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_ne.
+  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply oFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply oFunctor_map_compose.
 Qed.
 Instance gmapOF_contractive K `{Countable K} F :
   oFunctorContractive F → oFunctorContractive (gmapOF K F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, oFunctor_map_contractive.
 Qed.
 
 Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
@@ -649,18 +649,18 @@ Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := gmapO_map (rFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_ne.
+  by intros K ?? F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_ne.
 Qed.
 Next Obligation.
   intros K ?? F A ? B ? x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_map_compose.
 Qed.
 Instance gmapRF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply gmapO_map_ne, rFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index b631b236a0c185eaf10096497b01a46fdbb567a5..492ffe0b37e0d15fd97f44796f0174757d19ad7e 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -162,21 +162,21 @@ Program Definition listOF (F : oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_equiv_ext=>y. apply oFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_equiv_ext=>y; apply oFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance listOF_contractive F :
   oFunctorContractive F → oFunctorContractive (listOF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
 Qed.
 
 (* CMRA *)
@@ -550,19 +550,19 @@ Program Definition listURF (F : urFunctor) : urFunctor := {|
   urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance listURF_contractive F :
   urFunctorContractive F → urFunctorContractive (listURF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
 Qed.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 07b2993a16a0745c048bcac36d907b7832a3e29c..f13afb314feb9f2a8230fad13e6161542db9539d 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -689,22 +689,22 @@ Record oFunctor := OFunctor {
   oFunctor_car : ∀ A `{!Cofe A} B `{!Cofe B}, ofeT;
   oFunctor_map `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → oFunctor_car A1 B1 -n> oFunctor_car A2 B2;
-  oFunctor_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
+  oFunctor_map_ne `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :
     NonExpansive (@oFunctor_map A1 _ A2 _ B1 _ B2 _);
-  oFunctor_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
+  oFunctor_map_id `{!Cofe A, !Cofe B} (x : oFunctor_car A B) :
     oFunctor_map (cid,cid) x ≡ x;
-  oFunctor_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
+  oFunctor_map_compose `{!Cofe A1, !Cofe A2, !Cofe A3, !Cofe B1, !Cofe B2, !Cofe B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
     oFunctor_map (f◎g, g'◎f') x ≡ oFunctor_map (g,g') (oFunctor_map (f,f') x)
 }.
-Existing Instance oFunctor_ne.
+Existing Instance oFunctor_map_ne.
 Instance: Params (@oFunctor_map) 9 := {}.
 
 Delimit Scope oFunctor_scope with OF.
 Bind Scope oFunctor_scope with oFunctor.
 
 Class oFunctorContractive (F : oFunctor) :=
-  oFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
+  oFunctor_map_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Hint Mode oFunctorContractive ! : typeclass_instances.
 
@@ -732,12 +732,12 @@ Program Definition prodOF (F1 F2 : oFunctor) : oFunctor := {|
     prodO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_ne.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply prodO_map_ne; apply oFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !oFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [??]; rewrite /= !oFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [??]; simpl.
-  by rewrite !oFunctor_compose.
+  by rewrite !oFunctor_map_compose.
 Qed.
 Notation "F1 * F2" := (prodOF F1%OF F2%OF) : oFunctor_scope.
 
@@ -746,7 +746,7 @@ Instance prodOF_contractive F1 F2 :
   oFunctorContractive (prodOF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply prodO_map_ne; apply oFunctor_contractive.
+    by apply prodO_map_ne; apply oFunctor_map_contractive.
 Qed.
 
 Program Definition ofe_morOF (F1 F2 : oFunctor) : oFunctor := {|
@@ -756,15 +756,15 @@ Program Definition ofe_morOF (F1 F2 : oFunctor) : oFunctor := {|
 |}.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
-  apply ofe_morO_map_ne; apply oFunctor_ne; split; by apply Hfg.
+  apply ofe_morO_map_ne; apply oFunctor_map_ne; split; by apply Hfg.
 Qed.
 Next Obligation.
-  intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_id.
-  apply (ne_proper f). apply oFunctor_id.
+  intros F1 F2 A ? B ? [f ?] ?; simpl. rewrite /= !oFunctor_map_id.
+  apply (ne_proper f). apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [h ?] ?; simpl in *.
-  rewrite -!oFunctor_compose. do 2 apply (ne_proper _). apply oFunctor_compose.
+  rewrite -!oFunctor_map_compose. do 2 apply (ne_proper _). apply oFunctor_map_compose.
 Qed.
 Notation "F1 -n> F2" := (ofe_morOF F1%OF F2%OF) : oFunctor_scope.
 
@@ -773,7 +773,7 @@ Instance ofe_morOF_contractive F1 F2 :
   oFunctorContractive (ofe_morOF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n [f g] [f' g'] Hfg; simpl in *.
-  apply ofe_morO_map_ne; apply oFunctor_contractive; destruct n, Hfg; by split.
+  apply ofe_morO_map_ne; apply oFunctor_map_contractive; destruct n, Hfg; by split.
 Qed.
 
 (** * Sum type *)
@@ -848,12 +848,12 @@ Program Definition sumOF (F1 F2 : oFunctor) : oFunctor := {|
     sumO_map (oFunctor_map F1 fg) (oFunctor_map F2 fg)
 |}.
 Next Obligation.
-  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumO_map_ne; apply oFunctor_ne.
+  intros ?? A1 ? A2 ? B1 ? B2 ? n ???; by apply sumO_map_ne; apply oFunctor_map_ne.
 Qed.
-Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_id. Qed.
+Next Obligation. by intros F1 F2 A ? B ? [?|?]; rewrite /= !oFunctor_map_id. Qed.
 Next Obligation.
   intros F1 F2 A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' [?|?]; simpl;
-    by rewrite !oFunctor_compose.
+    by rewrite !oFunctor_map_compose.
 Qed.
 Notation "F1 + F2" := (sumOF F1%OF F2%OF) : oFunctor_scope.
 
@@ -862,7 +862,7 @@ Instance sumOF_contractive F1 F2 :
   oFunctorContractive (sumOF F1 F2).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n ???;
-    by apply sumO_map_ne; apply oFunctor_contractive.
+    by apply sumO_map_ne; apply oFunctor_map_contractive.
 Qed.
 
 (** * Discrete OFEs *)
@@ -1005,21 +1005,22 @@ Program Definition optionOF (F : oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := optionO_map (oFunctor_map F fg)
 |}.
 Next Obligation.
-  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_ne.
+  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_equiv_ext=>y; apply oFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_equiv_ext=>y; apply oFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Instance optionOF_contractive F :
   oFunctorContractive F → oFunctorContractive (optionOF F).
 Proof.
-  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply optionO_map_ne, oFunctor_contractive.
+  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg;
+    apply optionO_map_ne, oFunctor_map_contractive.
 Qed.
 
 (** * Later type *)
@@ -1113,22 +1114,22 @@ Program Definition laterOF (F : oFunctor) : oFunctor := {|
 |}.
 Next Obligation.
   intros F A1 ? A2 ? B1 ? B2 ? n fg fg' ?.
-  by apply (contractive_ne laterO_map), oFunctor_ne.
+  by apply (contractive_ne laterO_map), oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F A ? B ? x; simpl. rewrite -{2}(later_map_id x).
-  apply later_map_ext=>y. by rewrite oFunctor_id.
+  apply later_map_ext=>y. by rewrite oFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x; simpl. rewrite -later_map_compose.
-  apply later_map_ext=>y; apply oFunctor_compose.
+  apply later_map_ext=>y; apply oFunctor_map_compose.
 Qed.
 Notation "â–¶ F"  := (laterOF F%OF) (at level 20, right associativity) : oFunctor_scope.
 
 Instance laterOF_contractive F : oFunctorContractive (laterOF F).
 Proof.
   intros A1 ? A2 ? B1 ? B2 ? n fg fg' Hfg. apply laterO_map_contractive.
-  destruct n as [|n]; simpl in *; first done. apply oFunctor_ne, Hfg.
+  destruct n as [|n]; simpl in *; first done. apply oFunctor_map_ne, Hfg.
 Qed.
 
 (** * Dependently-typed functions over a discrete domain *)
@@ -1222,16 +1223,17 @@ Program Definition discrete_funOF {C} (F : C → oFunctor) : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := discrete_funO_map (λ c, oFunctor_map (F c) fg)
 |}.
 Next Obligation.
-  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g. by apply discrete_funO_map_ne=>?; apply oFunctor_ne.
+  intros C F A1 ? A2 ? B1 ? B2 ? n ?? g.
+  by apply discrete_funO_map_ne=>?; apply oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros C F A ? B ? g; simpl. rewrite -{2}(discrete_fun_map_id g).
-  apply discrete_fun_map_ext=> y; apply oFunctor_id.
+  apply discrete_fun_map_ext=> y; apply oFunctor_map_id.
 Qed.
 Next Obligation.
   intros C F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f1 f2 f1' f2' g.
   rewrite /= -discrete_fun_map_compose.
-  apply discrete_fun_map_ext=>y; apply oFunctor_compose.
+  apply discrete_fun_map_ext=>y; apply oFunctor_map_compose.
 Qed.
 
 Notation "T -d> F" := (@discrete_funOF T%type (λ _, F%OF)) : oFunctor_scope.
@@ -1240,7 +1242,7 @@ Instance discrete_funOF_contractive {C} (F : C → oFunctor) :
   (∀ c, oFunctorContractive (F c)) → oFunctorContractive (discrete_funOF F).
 Proof.
   intros ? A1 ? A2 ? B1 ? B2 ? n ?? g.
-  by apply discrete_funO_map_ne=>c; apply oFunctor_contractive.
+  by apply discrete_funO_map_ne=>c; apply oFunctor_map_contractive.
 Qed.
 
 (** * Constructing isomorphic OFEs *)
@@ -1503,16 +1505,16 @@ Section sigTOF.
     repeat intro. exists eq_refl => /=. solve_proper.
   Qed.
   Next Obligation.
-    simpl; intros. apply (existT_proper eq_refl), oFunctor_id.
+    simpl; intros. apply (existT_proper eq_refl), oFunctor_map_id.
   Qed.
   Next Obligation.
-    simpl; intros. apply (existT_proper eq_refl), oFunctor_compose.
+    simpl; intros. apply (existT_proper eq_refl), oFunctor_map_compose.
   Qed.
 
   Global Instance sigTOF_contractive {F} :
     (∀ a, oFunctorContractive (F a)) → oFunctorContractive (sigTOF F).
   Proof.
-    repeat intro. apply sigT_map => a. exact: oFunctor_contractive.
+    repeat intro. apply sigT_map => a. exact: oFunctor_map_contractive.
   Qed.
 End sigTOF.
 Arguments sigTOF {_} _%OF.
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index 3ec31e2238ae39054832c7a95ec7f22a04509193..a72c887bb918d58b4026a3a1b63ea0355ec660bf 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -92,7 +92,7 @@ Program Definition vecOF (F : oFunctor) m : oFunctor := {|
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := vecO_map m (oFunctor_map F fg)
 |}.
 Next Obligation.
-  intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_ne.
+  intros F A1 ? A2 ? B1 ? B2 ? n m f g Hfg. by apply vecO_map_ne, oFunctor_map_ne.
 Qed.
 Next Obligation.
   intros F m A ? B ? l.
@@ -103,11 +103,11 @@ Next Obligation.
   intros F m A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' l.
   change (vec_to_list (vec_map m (oFunctor_map F (f â—Ž g, g' â—Ž f')) l)
     ≡ vec_map m (oFunctor_map F (g, g')) (vec_map m (oFunctor_map F (f, f')) l)).
-  rewrite !vec_to_list_map. by apply: (oFunctor_compose (listOF F) f g f' g').
+  rewrite !vec_to_list_map. by apply: (oFunctor_map_compose (listOF F) f g f' g').
 Qed.
 
 Instance vecOF_contractive F m :
   oFunctorContractive F → oFunctorContractive (vecOF F m).
 Proof.
-  by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_contractive.
+  by intros ?? A1 ? A2 ? B1 ? B2 ? n ???; apply vecO_map_ne; first apply oFunctor_map_contractive.
 Qed.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 45fb5407c9553e0473aa302218d465c39d2f969c..8f4cb5cd6902a8ef116d7da60df95847077194ca 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -26,10 +26,10 @@ the agreement CMRA. *)
 category of CMRAs with a proof that it is locally contractive. *)
 Structure gFunctor := GFunctor {
   gFunctor_F :> rFunctor;
-  gFunctor_contractive : rFunctorContractive gFunctor_F;
+  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
 }.
 Arguments GFunctor _ {_}.
-Existing Instance gFunctor_contractive.
+Existing Instance gFunctor_map_contractive.
 Add Printing Constructor gFunctor.
 
 (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 2f6252b7e5d88267a5c35565f16b5734a7eea50d..d9cc45f05e96bd153ac9bef583f746fd8e7f3957 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -60,7 +60,7 @@ Section saved_anything.
     set (G1 := oFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := oFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
-    { intros z. rewrite /G1 /G2 -oFunctor_compose -{2}[z]oFunctor_id.
+    { intros z. rewrite /G1 /G2 -oFunctor_map_compose -{2}[z]oFunctor_map_id.
       apply (ne_proper (oFunctor_map F)); split=>?; apply iProp_fold_unfold. }
     rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
   Qed.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 2d7ce1524b0404281918a62df06f82dde81eae72..e602f4a933a562490cd3a249e99cf501133923bb 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -165,22 +165,22 @@ Program Definition uPredOF (F : urFunctor) : oFunctor := {|
 |}.
 Next Obligation.
   intros F A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
-  apply uPredO_map_ne, urFunctor_ne; split; by apply HPQ.
+  apply uPredO_map_ne, urFunctor_map_ne; split; by apply HPQ.
 Qed.
 Next Obligation.
   intros F A ? B ? P; simpl. rewrite -{2}(uPred_map_id P).
-  apply uPred_map_ext=>y. by rewrite urFunctor_id.
+  apply uPred_map_ext=>y. by rewrite urFunctor_map_id.
 Qed.
 Next Obligation.
   intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' P; simpl. rewrite -uPred_map_compose.
-  apply uPred_map_ext=>y; apply urFunctor_compose.
+  apply uPred_map_ext=>y; apply urFunctor_map_compose.
 Qed.
 
 Instance uPredOF_contractive F :
   urFunctorContractive F → oFunctorContractive (uPredOF F).
 Proof.
-  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ. apply uPredO_map_ne, urFunctor_contractive.
-  destruct n; split; by apply HPQ.
+  intros ? A1 ? A2 ? B1 ? B2 ? n P Q HPQ.
+  apply uPredO_map_ne, urFunctor_map_contractive. destruct n; split; by apply HPQ.
 Qed.
 
 (** logical entailement *)