From 5b8186e2f46d653e952236c4f2faf299581019b5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 09:58:48 +0200
Subject: [PATCH 1/5] Kill `{o,r,ur}Functor_diag` coercions.

---
 theories/algebra/cmra.v              |  2 --
 theories/algebra/cofe_solver.v       | 14 +++++++-------
 theories/algebra/ofe.v               |  8 ++------
 theories/base_logic/lib/iprop.v      |  6 ++++--
 theories/base_logic/lib/own.v        |  5 +++--
 theories/base_logic/lib/saved_prop.v |  6 +++---
 6 files changed, 19 insertions(+), 22 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index f2ed6b23c..18b38a614 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -802,7 +802,6 @@ Class rFunctorContractive (F : rFunctor) :=
 
 Definition rFunctor_diag (F: rFunctor) (A: ofeT) `{!Cofe A} : cmraT :=
   rFunctor_car F A A.
-Coercion rFunctor_diag : rFunctor >-> Funclass.
 
 Program Definition constRF (B : cmraT) : rFunctor :=
   {| rFunctor_car A1 _ A2 _ := B; rFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
@@ -840,7 +839,6 @@ Class urFunctorContractive (F : urFunctor) :=
 
 Definition urFunctor_diag (F: urFunctor) (A: ofeT) `{!Cofe A} : ucmraT :=
   urFunctor_car F A A.
-Coercion urFunctor_diag : urFunctor >-> Funclass.
 
 Program Definition constURF (B : ucmraT) : urFunctor :=
   {| urFunctor_car A1 _ A2 _ := B; urFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 2cb91a39a..968524403 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 (F solution_car _) solution_car;
+  solution_iso :> ofe_iso (oFunctor_diag 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 (F T _)}.
-Context `{Finh : Inhabited (F unitO _)}.
+Context `{Fcofe : ∀ (T : ofeT) `{!Cofe T}, Cofe (oFunctor_diag F T)}.
+Context `{Finh : Inhabited (oFunctor_diag 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) (F (projT1 (A' k)) (projT2 (A' k))) _
+  | S k => existT (P:=Cofe) (@oFunctor_diag 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 (F T _) :=
+Program Definition unfold_chain (X : T) : chain (oFunctor_diag 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) : F T _ := compl (unfold_chain X).
+Definition unfold (X : T) : oFunctor_diag 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 : F T _) : T :=
+Program Definition fold (X : oFunctor_diag 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 f8563361e..ab89ca16e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -710,10 +710,6 @@ Hint Mode oFunctorContractive ! : typeclass_instances.
 
 Definition oFunctor_diag (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
   oFunctor_car F A A.
-(** Note that the implicit argument [Cofe A] is not taken into account when
-[oFunctor_diag] is used as a coercion. So, given [F : oFunctor] and [A : ofeT]
-one has to write [F A _]. *)
-Coercion oFunctor_diag : oFunctor >-> Funclass.
 
 Program Definition constOF (B : ofeT) : oFunctor :=
   {| oFunctor_car A1 A2 _ _ := B; oFunctor_map A1 _ A2 _ B1 _ B2 _ f := cid |}.
@@ -1498,7 +1494,7 @@ Section sigTOF.
   Qed.
 
   Program Definition sigTOF (F : A → oFunctor) : oFunctor := {|
-    oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A _ B CB);
+    oFunctor_car A CA B CB := sigTO (λ a, oFunctor_car (F a) A B);
     oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := sigT_map (λ a, oFunctor_map (F a) fg)
   |}.
   Next Obligation.
@@ -1584,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 (F A _) (F B _) :=
+    (I : ofe_iso A B) : ofe_iso (oFunctor_diag F A) (oFunctor_diag 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 50169bddc..e3e52cefe 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -120,7 +120,8 @@ Module Type iProp_solution_sig.
   Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    discrete_funUR (λ i, gmapUR gname (gFunctors_lookup Σ i (iPrePropO Σ) _)).
+    discrete_funUR (λ i,
+      gmapUR gname (rFunctor_diag (gFunctors_lookup Σ i) (iPrePropO Σ))).
   Notation iProp Σ := (uPred (iResUR Σ)).
   Notation iPropO Σ := (uPredO (iResUR Σ)).
   Notation iPropI Σ := (uPredI (iResUR Σ)).
@@ -142,7 +143,8 @@ Module Export iProp_solution : iProp_solution_sig.
   Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
 
   Definition iResUR (Σ : gFunctors) : ucmraT :=
-    discrete_funUR (λ i, gmapUR gname (gFunctors_lookup Σ i (iPrePropO Σ) _)).
+    discrete_funUR (λ i,
+      gmapUR gname (rFunctor_diag (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 82553775f..4b1c3e312 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -9,14 +9,15 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
 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 = gFunctors_lookup Σ inG_id (iPrePropO Σ) _ }.
+  InG { inG_id : gid Σ; inG_prf :
+    A = rFunctor_diag (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 Σ (F (iPrePropO Σ) _).
+Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_diag 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 3ba56d398..8d3fff42a 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 (F (iPrePropO Σ) _));
+  saved_anything_inG :> inG Σ (agreeR (oFunctor_diag 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 : F (iPropO Σ) _) : iProp Σ :=
+    (γ : gname) (x : oFunctor_diag 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 : F (iPropO Σ) _.
+  Implicit Types x y : oFunctor_diag F (iPropO Σ).
   Implicit Types γ : gname.
 
   Global Instance saved_anything_persistent γ x :
-- 
GitLab


From 22b68d486031e1910e11e2dce19e7a7c4ed32647 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 18:22:29 +0200
Subject: [PATCH 2/5] Rename `{o,r,ur}Functor_diag` into
 `{o,r,ur}Functor_apply`.

---
 theories/algebra/cmra.v              |  4 ++--
 theories/algebra/cofe_solver.v       | 14 +++++++-------
 theories/algebra/ofe.v               |  4 ++--
 theories/base_logic/lib/iprop.v      |  4 ++--
 theories/base_logic/lib/own.v        |  4 ++--
 theories/base_logic/lib/saved_prop.v |  6 +++---
 6 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 18b38a614..b0f608cc5 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 968524403..f64b16654 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 ab89ca16e..e7197b7df 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 e3e52cefe..45fb5407c 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 4b1c3e312..357f2979e 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 8d3fff42a..2f6252b7e 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 :
-- 
GitLab


From 45b9c079cba99dcad694daf6205943066d9d6cf8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 09:59:35 +0200
Subject: [PATCH 3/5] CHANGELOG.

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 420d3949f..a8934aa4b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -81,6 +81,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
 * Add notion `ofe_iso A B` that states that OFEs `A` and `B` are isomorphic.
 * Make use of `ofe_iso` in the COFE solver.
+* The functions `{o,r,ur}Functor_diag` are no longer coercions, and renamed into
+  `{o,r,ur}Functor_apply` to better match their intent.
 
 **Changes in heap_lang:**
 
-- 
GitLab


From 6a295a21d60ea1a9bf6d469df2012b47a5122763 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 18:29:34 +0200
Subject: [PATCH 4/5] Comment about coercion.

---
 theories/algebra/ofe.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index e7197b7df..07b2993a1 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -708,6 +708,8 @@ Class oFunctorContractive (F : oFunctor) :=
     Contractive (@oFunctor_map F A1 _ A2 _ B1 _ B2 _).
 Hint Mode oFunctorContractive ! : typeclass_instances.
 
+(** Not a coercion due to the [Cofe] type class argument, and to avoid
+ambiguous coercion paths, see https://gitlab.mpi-sws.org/iris/iris/issues/240. *)
 Definition oFunctor_apply (F: oFunctor) (A: ofeT) `{!Cofe A} : ofeT :=
   oFunctor_car F A A.
 
-- 
GitLab


From 4326f5272ce595f93cda0fcafc81bf75bb435f0d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 18:35:57 +0200
Subject: [PATCH 5/5] Remove `-ambiguous-paths` option.

---
 _CoqProject | 2 --
 1 file changed, 2 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 900568c5e..d2742fd19 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,8 +8,6 @@
 -arg -w -arg -convert_concl_no_check
 # "Declare Scope" does not exist yet in 8.9.
 -arg -w -arg -undeclared-scope
-# We have ambiguous paths, and live with it.
--arg -w -arg -ambiguous-paths
 
 theories/algebra/monoid.v
 theories/algebra/cmra.v
-- 
GitLab