Adapt to rocq-prover/rocq#15802

Author: proux01

theories/Categories/Category/Morphisms.v

@@ -32,11 +32,14 @@ Hint Rewrite @left_inverse @right_inverse : morphism.
 Class Isomorphic {C : PreCategory} s d :=
   {
     morphism_isomorphic : morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+    isisomorphism_isomorphic : IsIsomorphism morphism_isomorphic
   }.
 
 (*Coercion Build_Isomorphic : IsIsomorphism >-> Isomorphic.*)
 Coercion morphism_isomorphic : Isomorphic >-> morphism.
+(* Use :> and remove the two following lines,
+   once Coq 8.16 is the minimum required version. *)
+#[export] Existing Instance isisomorphism_isomorphic.
 Coercion isisomorphism_isomorphic : Isomorphic >-> IsIsomorphism.
 
 Local Infix "<~=~>" := Isomorphic : category_scope.

theories/Colimits/Colimit.v

@@ -15,10 +15,12 @@ Generalizable All Variables.
 (** A colimit is the extremity of a cocone. *)
 
 Class IsColimit `(D: Diagram G) (Q: Type) := {
-  iscolimit_cocone :> Cocone D Q;
+  iscolimit_cocone : Cocone D Q;
   iscolimit_unicocone : UniversalCocone iscolimit_cocone;
 }.
-
+(* Use :> and remove the two following lines,
+   once Coq 8.16 is the minimum required version. *)
+#[export] Existing Instance iscolimit_cocone.
 Coercion iscolimit_cocone : IsColimit >-> Cocone.
 
 Arguments Build_IsColimit {G D Q} C H : rename.

theories/Diagrams/Cocone.v

@@ -83,9 +83,11 @@ Section Cocone.
   (** A cocone [C] over [D] to [X] is said universal when for all [Y] the map [cocone_postcompose] is an equivalence. In particular, given another cocone [C'] over [D] to [X'] the inverse of the map allows to recover a map [h] : [X] -> [X'] such that [C'] is [C] postcomposed with [h]. The fact that [cocone_postcompose] is an equivalence is an elegant way of stating the usual "unique existence" of category theory. *)
 
   Class UniversalCocone (C : Cocone D X) := {
-    is_universal :> forall Y, IsEquiv (@cocone_postcompose C Y);
+    is_universal : forall Y, IsEquiv (@cocone_postcompose C Y);
   }.
-
+  (* Use :> and remove the two following lines,
+     once Coq 8.16 is the minimum required version. *)
+  #[export] Existing Instance is_universal.
   Coercion is_universal : UniversalCocone >-> Funclass.
 
 End Cocone.

theories/Diagrams/Cone.v

@@ -81,9 +81,11 @@ Section Cone.
   (** A cone [C] over [D] from [X] is said universal when for all [Y] the map [cone_precompose] is an equivalence. In particular, given another cone [C'] over [D] from [X'] the inverse of the map allows us to recover a map [h] : [X] -> [X'] such that [C'] is [C] precomposed with [h]. The fact that [cone_precompose] is an equivalence is an elegant way of stating the usual "unique existence" of category theory. *)
 
   Class UniversalCone (C : Cone X D) := {
-    is_universal :> forall Y, IsEquiv (@cone_precompose C Y);
-  }.
-
+    is_universal : forall Y, IsEquiv (@cone_precompose C Y);
+    }.
+  (* Use :> and remove the two following lines,
+     once Coq 8.16 is the minimum required version. *)
+  #[export] Existing Instance is_universal.
   Coercion is_universal : UniversalCone >-> Funclass.
 
 End Cone.

theories/Limits/Limit.v

@@ -15,10 +15,12 @@ Generalizable All Variables.
 (** A Limit is the extremity of a cone. *)
 
 Class IsLimit `(D : Diagram G) (Q : Type) := {
-  islimit_cone :> Cone Q D;
+  islimit_cone : Cone Q D;
   islimit_unicone : UniversalCone islimit_cone;
 }.
-
+(* Use :> and remove the two following lines,
+   once Coq 8.16 is the minimum required version. *)
+#[export] Existing Instance islimit_cone.
 Coercion islimit_cone : IsLimit >-> Cone.
 
 Arguments Build_IsLimit {G D Q} C H : rename.