Revert (most of) rocq-prover#15802

As discussion in rocq-prover#15802 indicates we
should revert most fo this and rather go for the plan in
rocq-prover#16224 implemented by
rocq-prover#16230

Author: proux01

doc/sphinx/addendum/type-classes.rst

@@ -274,20 +274,12 @@ This declares singleton classes for reflexive and transitive relations,
 (see the :ref:`singleton class <singleton-class>` variant for an
 explanation). These may be used as parts of other classes:
 
-.. coqtop:: none
-
-   Set Warnings "-future-coercion-class-field".
-
 .. coqtop:: all
 
    Class PreOrder (A : Type) (R : relation A) :=
      { PreOrder_Reflexive :> Reflexive A R ;
        PreOrder_Transitive :> Transitive A R }.
 
-.. coqtop:: none
-
-   Set Warnings "+future-coercion-class-field".
-
 The syntax ``:>`` indicates that each ``PreOrder`` can be seen as a
 ``Reflexive`` relation. So each time a reflexive relation is needed, a
 preorder can be used instead. This is very similar to the coercion
@@ -340,17 +332,6 @@ Summary of the commands
 
          This command has no effect when used on a typeclass.
 
-.. _warn-future-coercion-class-field:
-
-   .. warn:: A coercion will be introduced in future versions when using ':>' in 'Class' declarations. Use '#[global] Existing Instance field.' instead if you don't want the coercion.
-
-      In future versions, :g:`:>` will also
-      declare a :ref:`coercion<coercions>`, as it does
-      for other :cmd:`Record` commands.
-      To eliminate the warning or to avoid creating the coercion
-      in the future, use :cmd:`Existing Instance` or :cmd:`Coercion` separately rather
-      than :g:`:>`.
-
    .. warn:: Ignored instance declaration for “@ident”: “@term” is not a class
 
       Using this ``:>`` syntax with a right-hand-side that is not itself a Class

doc/sphinx/changes.rst

@@ -331,13 +331,11 @@ Commands and options
   (`#15760 <https://github.com/coq/coq/pull/15760>`_,
   by Pierre Roux).
 - **Added:**
-  A deprecation warning that :n:`>` in a field of a :cmd:`Class`
-  and the :g:`Class >` syntax will in the future also
-  declare :ref:`coercions <coercions>` as they do when used in
+  A deprecation warning that the :g:`Class >` syntax, that is currently
+  doing nothing, will in the future
+  declare :ref:`coercions <coercions>` as it does when used in
   :cmd:`Record` commands
   (`#15802 <https://github.com/coq/coq/pull/15802>`_,
-  addresses `#2643 <https://github.com/coq/coq/issues/2643>`_
-  and `#9014 <https://github.com/coq/coq/issues/9014>`_,
   by Pierre Roux, reviewed by Gaëtan Gilbert, Ali Caglayan,
   Jason Gross, Jim Fehrle and Théo Zimmermann).
 - **Added:**

doc/sphinx/language/core/records.rst

@@ -91,7 +91,6 @@ Defining record types
        If specified, the field is declared as a coercion from the record name
        to the class of the field type. See :ref:`coercions`.
        Note that this currently does something else in :cmd:`Class` commands.
-       See :ref:`warning in Class <warn-future-coercion-class-field>`.
 
      - :n:`{+ @binder } : @of_type` is equivalent to
        :n:`: forall {+ @binder } , @of_type`

theories/Classes/CRelationClasses.v

@@ -70,18 +70,14 @@ Section Defs.
   (** A [PreOrder] is both Reflexive and Transitive. *)
 
   Class PreOrder (R : crelation A)  := {
-    PreOrder_Reflexive : Reflexive R | 2 ;
-    PreOrder_Transitive : Transitive R | 2 }.
-  #[global] Existing Instance PreOrder_Reflexive.
-  #[global] Existing Instance PreOrder_Transitive.
+    PreOrder_Reflexive :> Reflexive R | 2 ;
+    PreOrder_Transitive :> Transitive R | 2 }.
 
   (** A [StrictOrder] is both Irreflexive and Transitive. *)
 
   Class StrictOrder (R : crelation A)  := {
-    StrictOrder_Irreflexive : Irreflexive R ;
-    StrictOrder_Transitive : Transitive R }.
-  #[global] Existing Instance StrictOrder_Irreflexive.
-  #[global] Existing Instance StrictOrder_Transitive.
+    StrictOrder_Irreflexive :> Irreflexive R ;
+    StrictOrder_Transitive :> Transitive R }.
 
   (** By definition, a strict order is also asymmetric *)
   Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R.
@@ -90,20 +86,15 @@ Section Defs.
   (** A partial equivalence crelation is Symmetric and Transitive. *)
 
   Class PER (R : crelation A)  := {
-    PER_Symmetric : Symmetric R | 3 ;
-    PER_Transitive : Transitive R | 3 }.
-  #[global] Existing Instance PER_Symmetric.
-  #[global] Existing Instance PER_Transitive.
+    PER_Symmetric :> Symmetric R | 3 ;
+    PER_Transitive :> Transitive R | 3 }.
 
   (** Equivalence crelations. *)
 
   Class Equivalence (R : crelation A)  := {
-    Equivalence_Reflexive : Reflexive R ;
-    Equivalence_Symmetric : Symmetric R ;
-    Equivalence_Transitive : Transitive R }.
-  #[global] Existing Instance Equivalence_Reflexive.
-  #[global] Existing Instance Equivalence_Symmetric.
-  #[global] Existing Instance Equivalence_Transitive.
+    Equivalence_Reflexive :> Reflexive R ;
+    Equivalence_Symmetric :> Symmetric R ;
+    Equivalence_Transitive :> Transitive R }.
 
   (** An Equivalence is a PER plus reflexivity. *)
 

theories/Classes/RelationClasses.v

@@ -60,18 +60,14 @@ Section Defs.
   (** A [PreOrder] is both Reflexive and Transitive. *)
 
   Class PreOrder (R : relation A) : Prop := {
-    PreOrder_Reflexive : Reflexive R | 2 ;
-    PreOrder_Transitive : Transitive R | 2 }.
-  #[global] Existing Instance PreOrder_Reflexive.
-  #[global] Existing Instance PreOrder_Transitive.
+    PreOrder_Reflexive :> Reflexive R | 2 ;
+    PreOrder_Transitive :> Transitive R | 2 }.
 
   (** A [StrictOrder] is both Irreflexive and Transitive. *)
 
   Class StrictOrder (R : relation A) : Prop := {
-    StrictOrder_Irreflexive : Irreflexive R ;
-    StrictOrder_Transitive : Transitive R }.
-  #[global] Existing Instance StrictOrder_Irreflexive.
-  #[global] Existing Instance StrictOrder_Transitive.
+    StrictOrder_Irreflexive :> Irreflexive R ;
+    StrictOrder_Transitive :> Transitive R }.
 
   (** By definition, a strict order is also asymmetric *)
   Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R.
@@ -80,20 +76,15 @@ Section Defs.
   (** A partial equivalence relation is Symmetric and Transitive. *)
 
   Class PER (R : relation A) : Prop := {
-    PER_Symmetric : Symmetric R | 3 ;
-    PER_Transitive : Transitive R | 3 }.
-  #[global] Existing Instance PER_Symmetric.
-  #[global] Existing Instance PER_Transitive.
+    PER_Symmetric :> Symmetric R | 3 ;
+    PER_Transitive :> Transitive R | 3 }.
 
   (** Equivalence relations. *)
 
   Class Equivalence (R : relation A) : Prop := {
-    Equivalence_Reflexive : Reflexive R ;
-    Equivalence_Symmetric : Symmetric R ;
-    Equivalence_Transitive : Transitive R }.
-  #[global] Existing Instance Equivalence_Reflexive.
-  #[global] Existing Instance Equivalence_Symmetric.
-  #[global] Existing Instance Equivalence_Transitive.
+    Equivalence_Reflexive :> Reflexive R ;
+    Equivalence_Symmetric :> Symmetric R ;
+    Equivalence_Transitive :> Transitive R }.
 
   (** An Equivalence is a PER plus reflexivity. *)
 

theories/Classes/SetoidClass.v

@@ -29,8 +29,7 @@ Require Export Coq.Classes.Morphisms.
 
 Class Setoid A := {
   equiv : relation A ;
-  setoid_equiv : Equivalence equiv }.
-#[global] Existing Instance setoid_equiv.
+  setoid_equiv :> Equivalence equiv }.
 
 (* Too dangerous instance *)
 (* Program Instance [ eqa : Equivalence A eqA ] =>  *)
@@ -136,8 +135,7 @@ Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
 Class PartialSetoid (A : Type) :=
-  { pequiv : relation A ; pequiv_prf : PER pequiv }.
-#[global] Existing Instance pequiv_prf.
+  { pequiv : relation A ; pequiv_prf :> PER pequiv }.
 
 (** Overloaded notation for partial setoid equivalence. *)
 

vernac/record.ml

@@ -937,13 +937,6 @@ let warn_future_coercion_class_constructor =
     ~default:CWarnings.AsError
     Pp.(fun () -> str "'Class >' currently does nothing. Use 'Class' instead.")
 
-(* deprecated in 8.16, to be removed at the end of the deprecation phase
-   (c.f., https://github.com/coq/coq/pull/15802 ) *)
-let warn_future_coercion_class_field =
-  CWarnings.create ~name:"future-coercion-class-field" ~category:"records" Pp.(fun () ->
-      str "A coercion will be introduced in future versions when using ':>' in 'Class' declarations. "
-      ++ str "Use '#[global] Existing Instance field.' instead if you don't want the coercion.")
-
 (* declaring structures, common data to refactor *)
 let class_structure udecl kind def ~template ~cumulative ~poly ~primitive_proj finite records =
   let template, impargs, params, univs, variances, data =
@@ -954,8 +947,6 @@ let class_structure udecl kind def ~template ~cumulative ~poly ~primitive_proj f
       CErrors.user_err (str "Mutual definitional classes are not handled.")
   in
   if is_coercion then warn_future_coercion_class_constructor ();
-  if List.exists (function (_, { rf_subclass = Vernacexpr.BackInstance; _ }) -> true | _ -> false) cfs then
-    warn_future_coercion_class_field ();
   let coers = List.map (fun (_, { rf_subclass; rf_reverse; rf_priority }) ->
       if rf_reverse <> None then
         Attributes.(unsupported_attributes