diff --git a/coq/workspace.ml b/coq/workspace.ml
index 175550e4..585f577a 100644
--- a/coq/workspace.ml
+++ b/coq/workspace.ml
@@ -156,7 +156,7 @@ let make ~cmdline ~implicit ~kind ~debug =
   in
   let require_libs =
     let rq_list =
-      if init then ((None, "Coq.Init.Prelude") :: require_libraries) @ libs
+      if init then ((None, "Stdlib.Init.Prelude") :: require_libraries) @ libs
       else require_libraries @ libs
     in
     List.map mk_require_from rq_list
diff --git a/test/CoqProject/_CoqProject b/test/CoqProject/_CoqProject
index 3bf09db5..73b8c6f8 100644
--- a/test/CoqProject/_CoqProject
+++ b/test/CoqProject/_CoqProject
@@ -3,6 +3,6 @@
 
 -arg -w -arg -local-declaration
 -arg -w -arg +non-primitive-record
--arg -rifrom -arg Coq.Lists -arg List
+-arg -rifrom -arg Stdlib.Lists -arg List
 
 test.v
diff --git a/test/compiler/basic/run.t b/test/compiler/basic/run.t
index 92387815..7f39aa5c 100644
--- a/test/compiler/basic/run.t
+++ b/test/compiler/basic/run.t
@@ -6,7 +6,7 @@ Describe the project
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -17,7 +17,7 @@ Compile a single file, don't generate a `.vo` file:
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -33,7 +33,7 @@ Compile a single file, generate a .vo file
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -53,7 +53,7 @@ Compile a dependent file
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -73,7 +73,7 @@ Compile both files
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -94,7 +94,7 @@ Compile a dependent file without the dep being built
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -131,7 +131,7 @@ Compile a file with all messages:
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -142,7 +142,7 @@ Compile a file with all messages:
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -172,7 +172,7 @@ Use two workspaces
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -180,7 +180,7 @@ Use two workspaces
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -197,7 +197,7 @@ Load the example plugin
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -210,7 +210,7 @@ Load the astdump plugin
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
@@ -235,7 +235,7 @@ We do the same for the goaldump plugin:
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
diff --git a/test/compiler/exit_code/run.t b/test/compiler/exit_code/run.t
index c7127987..d27c7722 100644
--- a/test/compiler/exit_code/run.t
+++ b/test/compiler/exit_code/run.t
@@ -7,7 +7,7 @@ Describe the environment:
   [message] Configuration loaded from ./_CoqProject
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 3 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
diff --git a/test/compiler/long_file/run.t b/test/compiler/long_file/run.t
index f94b793b..83302ca7 100644
--- a/test/compiler/long_file/run.t
+++ b/test/compiler/long_file/run.t
@@ -10,7 +10,7 @@ We now compile the challenging file:
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
-   - Modules [Coq.Init.Prelude] will be loaded by default
+   - Modules [Stdlib.Init.Prelude] will be loaded by default
    - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
diff --git a/test/serlib/genarg/extraction.v b/test/serlib/genarg/extraction.v
index ec92c845..a771e714 100644
--- a/test/serlib/genarg/extraction.v
+++ b/test/serlib/genarg/extraction.v
@@ -1,4 +1,4 @@
-Require Coq.extraction.Extraction.
+Require Stdlib.extraction.Extraction.
 
 Extraction Language Haskell.
 
diff --git a/test/serlib/genarg/libTactics.v b/test/serlib/genarg/libTactics.v
index 451a77ad..5f895f69 100644
--- a/test/serlib/genarg/libTactics.v
+++ b/test/serlib/genarg/libTactics.v
@@ -44,7 +44,7 @@
 
 Set Implicit Arguments.
 
-Require Import Coq.Lists.List.
+Require Import Stdlib.Lists.List.
 
 
 (* ********************************************************************** *)
@@ -370,7 +370,7 @@ Ltac fast_rm_inside E :=
     Note: the tactic [number_to_nat] is extended in [LibInt] to
     take into account the [int] type, alias for [Z]. *)
 
-Require Coq.Numbers.BinNums Coq.ZArith.BinInt.
+Require Stdlib.Numbers.BinNums Stdlib.ZArith.BinInt.
 
 Definition ltac_int_to_nat (x:BinInt.Z) : nat :=
   match x with
@@ -2519,7 +2519,7 @@ Tactic Notation "subst_eq" constr(E) :=
 (* ---------------------------------------------------------------------- *)
 (** ** Tactics to work with proof irrelevance *)
 
-Require Import Coq.Logic.ProofIrrelevance.
+Require Import Stdlib.Logic.ProofIrrelevance.
 
 (** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
     unification variable, and is thus a practical way to
@@ -3098,7 +3098,7 @@ Tactic Notation "cases_if'" :=
     [inductions E gen X1 .. XN] is a shorthand for
     [dependent induction E generalizing X1 .. XN]. *)
 
-Require Import Coq.Program.Equality.
+Require Import Stdlib.Program.Equality.
 
 Ltac inductions_post :=
   unfold eq' in *.
@@ -3189,7 +3189,7 @@ Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
     judgment that includes a counter for the maximal height
     (see LibTacticsDemos for an example) *)
 
-Require Import Coq.Arith.Compare_dec.
+Require Import Stdlib.Arith.Compare_dec.
 Require Import Lia.
 
 Lemma induct_height_max2 : forall n1 n2 : nat,
@@ -4166,7 +4166,7 @@ Tactic Notation "exists" "~" constr(T1) "," constr(T2) "," constr(T3) ","
     same as for light automation.
 
     Exception: use [subs*] instead of [subst*] if you
-    import the library [Coq.Classes.Equivalence]. *)
+    import the library [Stdlib.Classes.Equivalence]. *)
 
 Tactic Notation "equates" "*" constr(E) :=
    equates E; auto_star.
@@ -5007,7 +5007,7 @@ Open Scope nat_scope.
 
 (** [exists T1 ... TN, P] is a shorthand for
     [exists T1, ..., exists TN, P]. Note that
-    [Coq.Program.Syntax] already defines exists
+    [Stdlib.Program.Syntax] already defines exists
     for arity up to 4. *)
 
 Notation "'exists' x1 ',' P" :=
diff --git a/vendor/coq b/vendor/coq
index 6a2431e6..7fec4bd9 160000
--- a/vendor/coq
+++ b/vendor/coq
@@ -1 +1 @@
-Subproject commit 6a2431e6fa1f4a0bbee6d98c3b709aca781061d5
+Subproject commit 7fec4bd91f2873f98541b5ecf640e83369768c99