Turn require Coq depr warnings as error by default

dev/ci/user-overlays/21851-proux01-warnerror-require-coq.sh

@@ -0,0 +1 @@
+overlay rewriter https://github.com/proux01/rewriter rocq21851 21851

library/nametab.ml

@@ -104,7 +104,7 @@ let corelib_id = Id.of_string "Corelib"
 
 let warn_deprecated_dirpath_Coq =
   CWarnings.create ~name:"deprecated-dirpath-Coq"
-    ~category:Deprecation.Version.v9_0
+    ~category:Deprecation.Version.v9_0 ~default:AsError
     ~quickfix:(fun ~loc (old_id, new_id) -> [Quickfix.make ~loc new_id])
     (fun (old_id, new_id) ->
       Pp.(old_id ++ spc () ++ str "has been replaced by" ++ spc () ++ new_id ++ str "."))

test-suite/bugs/bug_4976.v

@@ -1,4 +1,4 @@
-Require Import Coq.Setoids.Setoid.
+From Corelib Require Import Setoid.
 Definition silly (n : nat) := True.
 Ltac silly :=
   lazymatch goal with

test-suite/output/Qf_stdlib.out

@@ -1,19 +1,19 @@
-File "./output/Qf_stdlib.v", line 16, characters 6-22:
+File "./output/Qf_stdlib.v", line 16, characters 42-58:
 Warning: Coq.Init.Nat.add has been replaced by Corelib.Init.Nat.add.
 [deprecated-dirpath-Coq,deprecated-since-9.0,deprecated,default]
 Quickfix:
-Replace File "./output/Qf_stdlib.v", line 16, characters 6-22 with Corelib.Init.Nat.add
+Replace File "./output/Qf_stdlib.v", line 16, characters 42-58 with Corelib.Init.Nat.add
 Nat.add : nat -> nat -> nat
 
 Nat.add is not universe polymorphic
 Arguments Nat.add (n m)%_nat_scope
 Nat.add is transparent
 Expands to: Constant Corelib.Init.Nat.add
 Declared in library Corelib.Init.Nat, line 47, characters 9-12
-File "./output/Qf_stdlib.v", line 17, characters 6-22:
+File "./output/Qf_stdlib.v", line 17, characters 42-58:
 Warning: Coq.Init.Nat.add has been replaced by Corelib.Init.Nat.add.
 [deprecated-dirpath-Coq,deprecated-since-9.0,deprecated,default]
 Quickfix:
-Replace File "./output/Qf_stdlib.v", line 17, characters 6-22 with Corelib.Init.Nat.add
+Replace File "./output/Qf_stdlib.v", line 17, characters 42-58 with Corelib.Init.Nat.add
 Nat.add
      : nat -> nat -> nat

test-suite/output/Qf_stdlib.v

@@ -13,5 +13,5 @@ Require Import Corelib.ssr.ssrbool.
 From Corelib Require Import ssreflect ssrbool.
 
 (* Note: this tests the two different lookup modes *)
-About Coq.Init.Nat.add.
-Check Coq.Init.Nat.add.
+#[warning="deprecated-dirpath-Coq"] About Coq.Init.Nat.add.
+#[warning="deprecated-dirpath-Coq"] Check Coq.Init.Nat.add.

vernac/loadpath.ml

@@ -265,7 +265,7 @@ let locate_qualified_library ?root qid :
 
 let warn_deprecated_missing_stdlib =
   CWarnings.create ~name:"deprecated-missing-stdlib"
-    ~category:Deprecation.Version.v9_0
+    ~category:Deprecation.Version.v9_0 ~default:AsError
     (fun qid ->
       Pp.(str "Loading Stdlib without prefix is deprecated." ++ spc ()
           ++ str "Use \"From Stdlib Require " ++ Libnames.pr_qualid qid

vernac/synterp.ml

@@ -254,7 +254,7 @@ end
 
 let warn_deprecated_from_Coq =
   CWarnings.create ~name:"deprecated-from-Coq"
-    ~category:Deprecation.Version.v9_0
+    ~category:Deprecation.Version.v9_0 ~default:AsError
     ~quickfix:(fun ~loc qid -> [Quickfix.make ~loc (Libnames.pr_qualid qid)])
     (fun (_qid : qualid) -> strbrk
         "\"From Coq\" has been replaced by \"From Stdlib\".")