Merge PR #16237: Revert (most of) #15802

Reviewed-by: Alizter
Ack-by: Zimmi48
Co-authored-by: Alizter <[email protected]>

Author: coqbot-app[bot]

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

@@ -788,13 +788,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.")
-
 (** [declare_class] will prepare and declare a [Class]. This is done in
    2 steps:
 
@@ -822,8 +815,6 @@ let warn_future_coercion_class_field =
 let declare_class ~univs params inds def data =
   let id, idbuild, rdata, is_coercion, coers, inhabitant_id = get_class_params data in
   if is_coercion then warn_future_coercion_class_constructor ();
-  if List.exists (fun pf -> pf <> None) coers then
-    warn_future_coercion_class_field ();
   let fields = rdata.DataR.fields in
   let map ind =
     let map decl b y = {