diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 18b38a6147fe882d7c793e7dcfca75a5e6dde587..b0f608cc58b6b1617f985a785ab302e26386ae88 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -800,7 +800,7 @@ Class rFunctorContractive (F : rFunctor) :=
   rFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@rFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
-Definition rFunctor_diag (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
+Definition rFunctor_apply (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
   rFunctor_car F A A.
 
 Program Definition constRF (B : cmraT) : rFunctor :=
@@ -837,7 +837,7 @@ Class urFunctorContractive (F : urFunctor) :=
   urFunctor_contractive `{!Cofe A1, !Cofe A2, !Cofe B1, !Cofe B2} :>
     Contractive (@urFunctor_map F A1 _ A2 _ B1 _ B2 _).
 
-Definition urFunctor_diag (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
+Definition urFunctor_apply (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
   urFunctor_car F A A.
 
 Program Definition constURF (B : ucmraT) : urFunctor :=
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 968524403dd92e727ec9c8e75cd074ba94f41585..f64b166540f9ff2986746d2599e09e1f51351546 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -4,20 +4,20 @@ Set Default Proof Using "Type".
 Record solution (F : oFunctor) := Solution {
   solution_car :> ofeT;
   solution_cofe : Cofe solution_car;
-  solution_iso :> ofe_iso (oFunctor_diag F solution_car) solution_car;
+  solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
 }.
 Existing Instance solution_cofe.
 
 Module solver. Section solver.
 Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
-Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (oFunctor_diag F T)}.
-Context `{Finh : Inhabited (oFunctor_diag F unitO)}.
+Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (oFunctor_apply F T)}.
+Context `{Finh : Inhabited (oFunctor_apply F unitO)}.
 Notation map := (oFunctor_map F).
 
 Fixpoint A' (k : nat) : { C : ofeT & Cofe C } :=
   match k with
   | 0 => existT (P:=Cofe) unitO _
-  | S k => existT (P:=Cofe) (@oFunctor_diag F (projT1 (A' k)) (projT2 (A' k))) _
+  | S k => existT (P:=Cofe) (@oFunctor_apply F (projT1 (A' k)) (projT2 (A' k))) _
   end.
 Notation A k := (projT1 (A' k)).
 Local Instance A_cofe k : Cofe (A k) := projT2 (A' k).
@@ -176,7 +176,7 @@ Proof.
   - rewrite (ff_tower k (i - S k) X). by destruct (Nat.sub_add _ _ _).
 Qed.
 
-Program Definition unfold_chain (X : T) : chain (oFunctor_diag F T) :=
+Program Definition unfold_chain (X : T) : chain (oFunctor_apply F T) :=
   {| chain_car n := map (project n,embed' n) (X (S n)) |}.
 Next Obligation.
   intros X n i Hi.
@@ -186,14 +186,14 @@ Next Obligation.
   rewrite f_S -oFunctor_compose.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
-Definition unfold (X : T) : oFunctor_diag F T := compl (unfold_chain X).
+Definition unfold (X : T) : oFunctor_apply F T := compl (unfold_chain X).
 Instance unfold_ne : NonExpansive unfold.
 Proof.
   intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
     (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
 Qed.
 
-Program Definition fold (X : oFunctor_diag F T) : T :=
+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)).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index ab89ca16e7c6fddc67c52acd6488f25de68af82d..e7197b7dfb0d7af302a10f6f174bb877ba5b1151 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -708,7 +708,7 @@ Class oFunctorContractive (F : oFunctor) :=
     Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Hint Mode oFunctorContractive ! : typeclass_instances.
 
-Definition oFunctor_diag (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
+Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
   oFunctor_car F A A.
 
 Program Definition constOF (B : ofeT) : oFunctor :=
@@ -1580,7 +1580,7 @@ Instance iso_ofe_trans_ne {A B C} : NonExpansive2 (iso_ofe_trans (A:=A) (B:=B) (
 Proof. intros n I1 I2 [] J1 J2 []; split; simpl; by f_equiv. Qed.
 
 Program Definition iso_ofe_cong (F : oFunctor) `{!Cofe A, !Cofe B}
-    (I : ofe_iso A B) : ofe_iso (oFunctor_diag F A) (oFunctor_diag F B) :=
+    (I : ofe_iso A B) : ofe_iso (oFunctor_apply F A) (oFunctor_apply F B) :=
   OfeIso (oFunctor_map F (ofe_iso_2 I, ofe_iso_1 I))
     (oFunctor_map F (ofe_iso_1 I, ofe_iso_2 I)) _ _.
 Next Obligation.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index e3e52cefe32992031d95507b98105266a4eeeef8..45fb5407c9553e0473aa302218d465c39d2f969c 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -121,7 +121,7 @@ Module Type iProp_solution_sig.
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     discrete_funUR (λ i,
-      gmapUR gname (rFunctor_diag (gFunctors_lookup Σ i) (iPrePropO Σ))).
+      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
   Notation iProp Σ := (uPred (iResUR Σ)).
   Notation iPropO Σ := (uPredO (iResUR Σ)).
   Notation iPropI Σ := (uPredI (iResUR Σ)).
@@ -144,7 +144,7 @@ Module Export iProp_solution : iProp_solution_sig.
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     discrete_funUR (λ i,
-      gmapUR gname (rFunctor_diag (gFunctors_lookup Σ i) (iPrePropO Σ))).
+      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
   Notation iProp Σ := (uPred (iResUR Σ)).
   Notation iPropO Σ := (uPredO (iResUR Σ)).
 
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 4b1c3e3127eb2020e52cfea04c7a14dea67792ca..357f2979e2877143d81fe06fa5dec31ddfba95ce 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -10,14 +10,14 @@ needed because Coq is otherwise unable to solve type class constraints due to
 higher-order unification problems. *)
 Class inG (Σ : gFunctors) (A : cmraT) :=
   InG { inG_id : gid Σ; inG_prf :
-    A = rFunctor_diag (gFunctors_lookup Σ inG_id) (iPrePropO Σ)}.
+    A = rFunctor_apply (gFunctors_lookup Σ inG_id) (iPrePropO Σ)}.
 Arguments inG_id {_ _} _.
 (** We use the mode [-] for [Σ] since there is always a unique [Σ]. We use the
 mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
 not want Coq to pick one arbitrarily. *)
 Hint Mode inG - ! : typeclass_instances.
 
-Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_diag F (iPrePropO Σ)).
+Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPrePropO Σ)).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 
 (** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 8d3fff42a9bc700145b8c052ddd4161050bd9217..2f6252b7e5d88267a5c35565f16b5734a7eea50d 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -9,7 +9,7 @@ Import uPred.
    saved whatever-you-like. *)
 
 Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
-  saved_anything_inG :> inG Σ (agreeR (oFunctor_diag F (iPrePropO Σ)));
+  saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPrePropO Σ)));
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
 Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
 Proof. solve_inG. Qed.
 
 Definition saved_anything_own `{!savedAnythingG Σ F}
-    (γ : gname) (x : oFunctor_diag F (iPropO Σ)) : iProp Σ :=
+    (γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
   own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
 Instance: Params (@saved_anything_own) 4 := {}.
 
 Section saved_anything.
   Context `{!savedAnythingG Σ F}.
-  Implicit Types x y : oFunctor_diag F (iPropO Σ).
+  Implicit Types x y : oFunctor_apply F (iPropO Σ).
   Implicit Types γ : gname.
 
   Global Instance saved_anything_persistent γ x :