diff --git a/src/Extract.v b/src/Extract.v
index 4f2319a..9322605 100644
--- a/src/Extract.v
+++ b/src/Extract.v
@@ -14,7 +14,7 @@
 (* 02110-1301 USA                                                     *)
 
 From Stalmarck Require Import algoRun.
-From Coq Require Import ZArith.
-From Coq Require Import Extraction.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Extraction.
 
 Extraction "stal.ml" run checkTracef zero Pos.of_succ_nat.
diff --git a/src/staltac_lib.ml b/src/staltac_lib.ml
index cf6c5df..ee58b83 100644
--- a/src/staltac_lib.ml
+++ b/src/staltac_lib.ml
@@ -31,7 +31,7 @@ let global_reference_in_absolute_module dir id =
   Nametab.global_of_path (Libnames.make_path dir id)
 
 let constant dir s =
-  let dir = DirPath.make (List.map Id.of_string (List.rev ("Coq"::dir))) in
+  let dir = DirPath.make (List.map Id.of_string (List.rev ("Corelib"::dir))) in
   let id = Id.of_string s in
   try
     EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Global.env ()) (global_reference_in_absolute_module dir id))
diff --git a/theories/Algorithm/BoolAux.v b/theories/Algorithm/BoolAux.v
index 0e2e0d4..7524348 100644
--- a/theories/Algorithm/BoolAux.v
+++ b/theories/Algorithm/BoolAux.v
@@ -21,7 +21,7 @@ Some standard properties of booleans.
 
 *)
 
-From Coq Require Export Bool.
+From Stdlib Require Export Bool.
 
 Lemma de_morgan1 : forall b1 b2 : bool, negb (b1 || b2) = negb b1 && negb b2.
 Proof.
diff --git a/theories/Algorithm/OrderedListEq.v b/theories/Algorithm/OrderedListEq.v
index fbbae86..ddcf23a 100644
--- a/theories/Algorithm/OrderedListEq.v
+++ b/theories/Algorithm/OrderedListEq.v
@@ -22,11 +22,11 @@ we took a special care so that every function can be evaluated
 inside Coq, see OrderedListEq_ex
 *)
 
-From Coq Require Import Arith.
-From Coq Require Export List.
-From Coq Require Import Lexicographic_Exponentiation.
-From Coq Require Export Relation_Definitions.
-From Coq Require Export Relation_Operators.
+From Stdlib Require Import Arith.
+From Stdlib Require Export List.
+From Stdlib Require Import Lexicographic_Exponentiation.
+From Stdlib Require Export Relation_Definitions.
+From Stdlib Require Export Relation_Operators.
 From Stalmarck Require Export sTactic.
 
 Section OrderedList.
diff --git a/theories/Algorithm/OrderedListEq_ex.v b/theories/Algorithm/OrderedListEq_ex.v
index 2a57732..9cd6e1a 100644
--- a/theories/Algorithm/OrderedListEq_ex.v
+++ b/theories/Algorithm/OrderedListEq_ex.v
@@ -21,7 +21,7 @@ How to use OrderedList
 *)
 
 From Stalmarck Require Import OrderedListEq.
-From Coq Require Import Arith. (* For Nat *)
+From Stdlib Require Import Arith. (* For Nat *)
 
 Definition CNat : forall a b : nat, {a < b} + {b < a} + {a = b}.
 fix CNat 1; intros a; case a; [ idtac | intros a' ]; intros b; case b;
@@ -58,7 +58,7 @@ Eval compute in (appnat l1 l2).
 Eval compute in (getminnat l1 l2).
 Eval compute in (internat l1 l2).
 
-From Coq Require Import ZArith. (* For Z *)
+From Stdlib Require Import ZArith. (* For Z *)
 
 Definition CZ : forall a b : Z, {(a < b)%Z} + {(b < a)%Z} + {a = b}.
 intros a b; CaseEq (a - b)%Z.
diff --git a/theories/Algorithm/PolyListAux.v b/theories/Algorithm/PolyListAux.v
index 892b667..e236fa9 100644
--- a/theories/Algorithm/PolyListAux.v
+++ b/theories/Algorithm/PolyListAux.v
@@ -20,8 +20,8 @@ Pierre Letouzey & Laurent Thery
 Definition of rem a function that removes elt from polymorphic lists
 *)
 
-From Coq Require Import Arith.
-From Coq Require Import List.
+From Stdlib Require Import Arith.
+From Stdlib Require Import List.
 
 Section Auxrem.
 Variable A : Type.
diff --git a/theories/Algorithm/algoRun.v b/theories/Algorithm/algoRun.v
index fade411..c37c1c8 100644
--- a/theories/Algorithm/algoRun.v
+++ b/theories/Algorithm/algoRun.v
@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Some examples of computing with stalmarck inside Coq
 *)
 
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 From Stalmarck Require Export algoStalmarck.
 From Stalmarck Require Export algoTrace.
 From Stalmarck Require Export makeTriplet.
diff --git a/theories/Algorithm/complete.v b/theories/Algorithm/complete.v
index f71e62b..195f754 100644
--- a/theories/Algorithm/complete.v
+++ b/theories/Algorithm/complete.v
@@ -174,7 +174,7 @@ rewrite (Hab1 f Abs Hf2); rewrite (rZEvalCompInv b f).
 case (rZEval f b); auto with bool stalmarck.
 Qed.
 
-From Coq Require Import Arith.
+From Stdlib Require Import Arith.
 
 Fixpoint nthTail (n : nat) : list rZ -> list rZ :=
   fun l : list rZ =>
diff --git a/theories/Algorithm/equalBefore.v b/theories/Algorithm/equalBefore.v
index 9379bb9..386d268 100644
--- a/theories/Algorithm/equalBefore.v
+++ b/theories/Algorithm/equalBefore.v
@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of equality on booleans up to a certain number
 *)
 
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Relation_Definitions.
 From Stalmarck Require Export triplet.
 
 (** f and g gives same value for rNat less than m *)
diff --git a/theories/Algorithm/interImplement2.v b/theories/Algorithm/interImplement2.v
index e5b7526..468e00c 100644
--- a/theories/Algorithm/interImplement2.v
+++ b/theories/Algorithm/interImplement2.v
@@ -23,7 +23,7 @@ Implement the intersection (2 files)
 From Stalmarck Require Import rZ.
 From Stalmarck Require Import OrderedListEq.
 From Stalmarck Require Import LetP.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Relation_Definitions.
 From Stalmarck Require Import state.
 From Stalmarck Require Import restrictState.
 From Stalmarck Require Import ltState.
diff --git a/theories/Algorithm/interImplement2_ex.v b/theories/Algorithm/interImplement2_ex.v
index f3e3e87..7f29a66 100644
--- a/theories/Algorithm/interImplement2_ex.v
+++ b/theories/Algorithm/interImplement2_ex.v
@@ -21,7 +21,7 @@ How to use our module on ordered list
 *)
 
 From Stalmarck Require Import interImplement2.
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 
 #[local] Definition A := rArrayInit _ (fun n : rNat => class nil).
 
diff --git a/theories/Algorithm/interState.v b/theories/Algorithm/interState.v
index 449c2f7..b36fde4 100644
--- a/theories/Algorithm/interState.v
+++ b/theories/Algorithm/interState.v
@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of the intersection of two states
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export stateDec.
 
 (** The property of being an intersection *)
diff --git a/theories/Algorithm/ltState.v b/theories/Algorithm/ltState.v
index 1163ec1..3488844 100644
--- a/theories/Algorithm/ltState.v
+++ b/theories/Algorithm/ltState.v
@@ -22,11 +22,11 @@ of valid equations where variables belong to a given list
 *)
 
 From Stalmarck Require Import state.
-From Coq Require Import Arith.
+From Stdlib Require Import Arith.
 From Stalmarck Require Import stateDec.
-From Coq Require Import Inverse_Image.
-From Coq Require Import Compare.
-From Coq Require Import Relation_Definitions.
+From Stdlib Require Import Inverse_Image.
+From Stdlib Require Import Compare.
+From Stdlib Require Import Relation_Definitions.
 
 Section lt.
 Variable L : list rNat.
diff --git a/theories/Algorithm/rZ.v b/theories/Algorithm/rZ.v
index ed30245..2c6b119 100644
--- a/theories/Algorithm/rZ.v
+++ b/theories/Algorithm/rZ.v
@@ -31,12 +31,12 @@ At the end we define functional arrays that will be used in implementation
 *)
 
 From Stalmarck Require Import sTactic.
-From Coq Require Import Relation_Definitions.
-From Coq Require Import ZArith.
-From Coq Require Import Inverse_Image.
-From Coq Require Import Inclusion.
-From Coq Require Import Wf_nat.
-From Coq Require Import List.
+From Stdlib Require Import Relation_Definitions.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import Inverse_Image.
+From Stdlib Require Import Inclusion.
+From Stdlib Require Import Wf_nat.
+From Stdlib Require Import List.
 
 Definition rNat := positive.
 
diff --git a/theories/Algorithm/refl.v b/theories/Algorithm/refl.v
index a3ee813..98692ee 100644
--- a/theories/Algorithm/refl.v
+++ b/theories/Algorithm/refl.v
@@ -20,9 +20,9 @@ Pierre Letouzey & Laurent Thery
 Construct a function of type [Expr -> Prop]
 *)
 
-From Coq Require Import ZArith.
+From Stdlib Require Import ZArith.
 From Stalmarck Require Import normalize.
-From Coq Require Import Classical.
+From Stdlib Require Import Classical.
 From Stalmarck Require Import sTactic.
 
 Section refl.
diff --git a/theories/Algorithm/state.v b/theories/Algorithm/state.v
index d93d366..284e438 100644
--- a/theories/Algorithm/state.v
+++ b/theories/Algorithm/state.v
@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of states as the list of equations, i.e., pairs of rZ
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export triplet.
 
 Definition State := list (rZ * rZ).
diff --git a/theories/Algorithm/stateDec.v b/theories/Algorithm/stateDec.v
index 2c364db..4219d4b 100644
--- a/theories/Algorithm/stateDec.v
+++ b/theories/Algorithm/stateDec.v
@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Given a state, equality is decidable
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export state.
 
 (** To show that the equality is decidable we need a more `constructive' predicate
diff --git a/theories/Algorithm/triplet.v b/theories/Algorithm/triplet.v
index 026e894..6c31544 100644
--- a/theories/Algorithm/triplet.v
+++ b/theories/Algorithm/triplet.v
@@ -20,9 +20,9 @@ Pierre Letouzey & Laurent Thery
 Definition of triplets
 *)
 
-From Coq Require Export Bool.
+From Stdlib Require Export Bool.
 From Stalmarck Require Export rZ.
-From Coq Require Export List.
+From Stdlib Require Export List.
 From Stalmarck Require Export normalize.
 From Stalmarck Require Export sTactic.
 
diff --git a/theories/Algorithm/unionState.v b/theories/Algorithm/unionState.v
index 046ebd5..c342c28 100644
--- a/theories/Algorithm/unionState.v
+++ b/theories/Algorithm/unionState.v
@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 Definition of the union of two states
 *)
 
-From Coq Require Import List.
+From Stdlib Require Import List.
 From Stalmarck Require Export state.
 
 (** The property of being an union *)
diff --git a/theories/Algorithm/wfArray.v b/theories/Algorithm/wfArray.v
index 68636de..37e5eba 100644
--- a/theories/Algorithm/wfArray.v
+++ b/theories/Algorithm/wfArray.v
@@ -22,10 +22,10 @@ Define a notion of wellformedness of function arrays for our application
 
 From Stalmarck Require Export rZ.
 From Stalmarck Require Export OrderedListEq.
-From Coq Require Export Relation_Definitions.
+From Stdlib Require Export Relation_Definitions.
 From Stalmarck Require Export LetP.
 From Stalmarck Require Export PolyListAux.
-From Coq Require Export List.
+From Stdlib Require Export List.
 From Stalmarck Require Export sTactic.
 
 (** Definition of well formed array and some properties *)
diff --git a/theories/Tactic/StalTac.v b/theories/Tactic/StalTac.v
index 5c43373..0d14f87 100644
--- a/theories/Tactic/StalTac.v
+++ b/theories/Tactic/StalTac.v
@@ -20,7 +20,7 @@ Pierre Letouzey & Laurent Thery
 A wrapper for the stalmarck tactic
 *)
 
-From Coq Require Export ZArith.
+From Stdlib Require Export ZArith.
 From Stalmarck Require Export normalize.
 From Stalmarck Require Export algoTrace.
 From Stalmarck Require Export refl.
diff --git a/theories/Tactic/StalTac_ex.v b/theories/Tactic/StalTac_ex.v
index ec55a9c..40f6916 100644
--- a/theories/Tactic/StalTac_ex.v
+++ b/theories/Tactic/StalTac_ex.v
@@ -21,7 +21,7 @@ Examples for the stalmarck tactic
 *)
 
 From Stalmarck Require Import StalTac.
-From Coq Require Import Classical.
+From Stdlib Require Import Classical.
 
 Theorem Praeclarum :
  forall x y z t : Prop, (x -> z) /\ (y -> t) -> x /\ y -> z /\ t.