diff --git a/dev/ci/user-overlays/21851-proux01-warnerror-require-coq.sh b/dev/ci/user-overlays/21851-proux01-warnerror-require-coq.sh
new file mode 100644
index 000000000000..49037cfeaf15
--- /dev/null
+++ b/dev/ci/user-overlays/21851-proux01-warnerror-require-coq.sh
@@ -0,0 +1 @@
+overlay rewriter https://github.com/proux01/rewriter rocq21851 21851
diff --git a/library/nametab.ml b/library/nametab.ml
index b149fe692b65..798b563e2434 100644
--- a/library/nametab.ml
+++ b/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 "."))
diff --git a/test-suite/bugs/bug_4976.v b/test-suite/bugs/bug_4976.v
index 18e6b8d476d4..04ef6dfd2e13 100644
--- a/test-suite/bugs/bug_4976.v
+++ b/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
diff --git a/test-suite/output/Qf_stdlib.out b/test-suite/output/Qf_stdlib.out
index 31c209f7c08b..38bcd6f43951 100644
--- a/test-suite/output/Qf_stdlib.out
+++ b/test-suite/output/Qf_stdlib.out
@@ -1,8 +1,8 @@
-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
@@ -10,10 +10,10 @@ 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
diff --git a/test-suite/output/Qf_stdlib.v b/test-suite/output/Qf_stdlib.v
index 05d8be359d0d..f83e6262db17 100644
--- a/test-suite/output/Qf_stdlib.v
+++ b/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.
diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index 4b6ef278414c..dd08f5689e31 100644
--- a/vernac/loadpath.ml
+++ b/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
diff --git a/vernac/synterp.ml b/vernac/synterp.ml
index 712480ac7c5e..e16d8fab6a34 100644
--- a/vernac/synterp.ml
+++ b/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\".")