Turn warnings about :> in Class as error

This way, in next version, we can finally have :> declare a coercion
in any record declaration, including typeclasses. Whereas ::
consistently declares typeclass instances since Coq 8.18.

Author: proux01

doc/changelog/02-specification-language/18590-cleanup_16230.rst

@@ -0,0 +1,51 @@
+- **Changed:**
+  warnings `future-coercion-class-constructor`
+  and `future-coercion-class-field` about ``:>`` in :cmd:`Class` as
+  error by default. This offers a last opportunity to replace ``:>``
+  with ``::`` (available since Coq 8.18) to declare typeclass instances
+  before making ``:>`` consistently declare coercions in all records in
+  next version.
+  To adapt huge codebases, you can try
+  `this script <https://gist.github.com/JasonGross/59fc3c03664f2280849abf50b531be42>`_
+  or the one below. But beware that both are incomplete.
+
+  .. code-block:: sh
+
+     #!/bin/awk -f
+     BEGIN {
+       startclass = 0;
+       inclass = 0;
+       indefclass = 0;  # definitionalclasses (single field, without { ... })
+     }
+     {
+       if ($0 ~ "[ ]*Class") {
+         startclass = 1;
+       }
+       if (startclass == 1 && $0 ~ ":=") {
+         inclass = 1;
+         indefclass = 1;
+       }
+       if (startclass == 1 && $0 ~ ":=.*{") {
+         indefclass = 0;
+       }
+       if (inclass == 1) startclass = 0;
+
+       if (inclass == 1 && $0 ~ ":>") {
+         if ($0 ~ "{ .*:>") {  # first field on a single line
+           sub("{ ", "{ #[global] ");
+         } else if ($0 ~ ":=.*:>") {  # definitional classes on a single line
+           sub(":= ", ":= #[global] ");
+         } else if ($0 ~ "^  ") {
+           sub("  ", "  #[global] ");
+         } else {
+           $0 = "#[global] " $0;
+         }
+         sub(":>", "::")
+       }
+     print $0;
+
+     if ($0 ~ ".*}[.]" || indefclass == 1 && $0 ~ "[.]$") inclass = 0;
+   }
+
+  (`#18590 <https://github.com/coq/coq/pull/18590>`_,
+  by Pierre Roux).

doc/sphinx/addendum/type-classes.rst

@@ -248,7 +248,7 @@ the implicit arguments mechanism if available, as shown in the example.
 Substructures
 ~~~~~~~~~~~~~
 
-.. index:: :> (substructure)
+.. index:: :: (substructure)
 
 Substructures are components of a typeclass which are themselves instances of a
 typeclass. They often arise when using typeclasses for logical properties, e.g.:

vernac/record.ml

@@ -679,6 +679,7 @@ let warn_future_coercion_class_constructor =
    (c.f., https://github.com/coq/coq/pull/16230 ) *)
 let warn_future_coercion_class_field =
   CWarnings.create ~name:"future-coercion-class-field" ~category:Deprecation.Version.v8_17
+    ~default:CWarnings.AsError
     Pp.(fun definitional ->
     strbrk "A coercion will be introduced instead of an instance in future versions when using ':>' in 'Class' declarations. "
     ++ strbrk "Replace ':>' with '::' (or use '#[global] Existing Instance field.' for compatibility with Coq < 8.18). Beware that the default locality for '::' is #[export], as opposed to #[global] for ':>' currently."