diff --git a/BigN/BigN.v b/BigN/BigN.v
index b1c0c93..fff3d4b 100644
--- a/BigN/BigN.v
+++ b/BigN/BigN.v
@@ -10,8 +10,8 @@
 
 (** Initial Author: Arnaud Spiwack *)
 
-Require Import Lia CyclicAxioms Ring63 NSig NSigNAxioms NMake
-  NProperties GenericMinMax.
+From Stdlib Require Import Lia CyclicAxioms Ring63 NProperties GenericMinMax.
+Require Import NSig NSigNAxioms NMake.
 Import Cyclic63.
 
 (** The following [BigN] module regroups both the operations and
@@ -44,7 +44,7 @@ Notation bigN := BigN.t.
 Bind Scope bigN_scope with bigN.
 Bind Scope bigN_scope with BigN.t.
 Bind Scope bigN_scope with BigN.t'.
-Arguments BigN.N0 _%int63.
+Arguments BigN.N0 _%_int63.
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
 Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
diff --git a/BigN/NMake.v b/BigN/NMake.v
index 66f8be1..cfba61b 100644
--- a/BigN/NMake.v
+++ b/BigN/NMake.v
@@ -16,8 +16,9 @@
     representation. The representation-dependent (and macro-generated) part
     is now in [NMake_gen]. *)
 
-Require Import Bool BigNumPrelude ZArith Lia Nnat CyclicAxioms DoubleType
-  Nbasic Wf_nat StreamMemo NSig NMake_gen.
+From Stdlib Require Import Bool ZArith Lia Nnat CyclicAxioms DoubleType.
+From Stdlib Require Import Wf_nat StreamMemo.
+Require Import BigNumPrelude Nbasic NSig NMake_gen.
 
 Module Make (W0:CyclicType) <: NType.
 
diff --git a/BigN/Nbasic.v b/BigN/Nbasic.v
index 5e90137..ac2ebee 100644
--- a/BigN/Nbasic.v
+++ b/BigN/Nbasic.v
@@ -8,11 +8,11 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
+From Stdlib Require Import CyclicAxioms.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
-Require Import CyclicAxioms.
 Require Import DoubleCyclic.
 
 Arguments mk_zn2z_ops [t] ops.
diff --git a/BigN/gen/NMake_gen.ml b/BigN/gen/NMake_gen.ml
index e89e17b..4b3db11 100644
--- a/BigN/gen/NMake_gen.ml
+++ b/BigN/gen/NMake_gen.ml
@@ -49,9 +49,9 @@ pr
 
 (** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)
 
-Require Import BigNumPrelude ZArith Lia CyclicAxioms
- DoubleType DoubleMul DoubleDivn1 DoubleBase DoubleCyclic Nbasic
- Wf_nat StreamMemo.
+From Stdlib Require Import ZArith Lia CyclicAxioms DoubleType Wf_nat StreamMemo.
+Require Import BigNumPrelude.
+Require Import DoubleMul DoubleDivn1 DoubleBase DoubleCyclic Nbasic.
 
 Local Close Scope Z.
 
diff --git a/BigNumPrelude.v b/BigNumPrelude.v
index b629a39..1708ebd 100644
--- a/BigNumPrelude.v
+++ b/BigNumPrelude.v
@@ -14,14 +14,14 @@
     numbers. *)
 
 
-Require Import ArithRing.
-Require Export ZArith.
-Require Export Znumtheory.
-Require Export Zpow_facts.
-Require Uint63.
-Require Import Lia.
-
-Declare ML Module "bignums_syntax_plugin:coq-bignums.plugin".
+From Stdlib Require Import ArithRing.
+From Stdlib Require Export ZArith.
+From Stdlib Require Export Znumtheory.
+From Stdlib Require Export Zpow_facts.
+From Stdlib Require Uint63.
+From Stdlib Require Import Lia.
+
+Declare ML Module "coq-bignums.plugin".
 
 (* *** Nota Bene ***
    All results that were general enough have been moved in ZArith.
diff --git a/BigQ/BigQ.v b/BigQ/BigQ.v
index ab0e8fd..145ae72 100644
--- a/BigQ/BigQ.v
+++ b/BigQ/BigQ.v
@@ -10,8 +10,9 @@
 
 (** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
 
+From Stdlib Require Import Field Qfield Orders GenericMinMax.
 Require Export BigZ.
-Require Import Field Qfield QSig QMake Orders GenericMinMax.
+Require Import QSig QMake.
 
 (** We choose for BigQ an implemention with
     multiple representation of 0: 0, 1/0, 2/0 etc.
diff --git a/BigQ/QMake.v b/BigQ/QMake.v
index cb8cfcb..ad1d128 100644
--- a/BigQ/QMake.v
+++ b/BigQ/QMake.v
@@ -10,9 +10,9 @@
 
 (** Initial authors : Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
 
-Require Import BigNumPrelude Lia.
-Require Import QArith Qcanon Qpower Qminmax.
-Require Import NSig ZSig QSig.
+From Stdlib Require Import Lia.
+From Stdlib Require Import QArith Qcanon Qpower Qminmax.
+Require Import BigNumPrelude NSig ZSig QSig.
 
 (** We will build rationals out of an implementation of integers [ZType]
     for numerators and an implementation of natural numbers [NType] for
diff --git a/BigZ/BigZ.v b/BigZ/BigZ.v
index 0582395..68cce96 100644
--- a/BigZ/BigZ.v
+++ b/BigZ/BigZ.v
@@ -8,8 +8,9 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
+From Stdlib Require Import ZProperties ZDivFloor Ring Lia.
 Require Export BigN.
-Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake Ring Lia.
+Require Import ZSig ZSigZAxioms ZMake.
 Import Zpow_def Zdiv.
 
 (** * [BigZ] : arbitrary large efficient integers.
@@ -45,8 +46,8 @@ Notation bigZ := BigZ.t.
 Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
-Arguments BigZ.Pos _%bigN.
-Arguments BigZ.Neg _%bigN.
+Arguments BigZ.Pos _%_bigN.
+Arguments BigZ.Neg _%_bigN.
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
 Local Notation "2" := BigZ.two : bigZ_scope.
diff --git a/BigZ/ZMake.v b/BigZ/ZMake.v
index b892fb6..ca188d8 100644
--- a/BigZ/ZMake.v
+++ b/BigZ/ZMake.v
@@ -8,7 +8,7 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
 Require Import BigNumPrelude.
 Require Import NSig.
 Require Import ZSig.
diff --git a/CyclicDouble/DoubleAdd.v b/CyclicDouble/DoubleAdd.v
index 1664f22..5f1e245 100644
--- a/CyclicDouble/DoubleAdd.v
+++ b/CyclicDouble/DoubleAdd.v
@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
diff --git a/CyclicDouble/DoubleBase.v b/CyclicDouble/DoubleBase.v
index 3959a98..4bf1de7 100644
--- a/CyclicDouble/DoubleBase.v
+++ b/CyclicDouble/DoubleBase.v
@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith.
+From Stdlib Require Import ZArith.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 
 Local Open Scope Z_scope.
 
@@ -441,4 +441,3 @@ Section DoubleBase.
  End DoubleProof.
 
 End DoubleBase.
-
diff --git a/CyclicDouble/DoubleCyclic.v b/CyclicDouble/DoubleCyclic.v
index 4ccc19a..fff3073 100644
--- a/CyclicDouble/DoubleCyclic.v
+++ b/CyclicDouble/DoubleCyclic.v
@@ -10,9 +10,10 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
+From Stdlib Require Import CyclicAxioms.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 Require Import DoubleAdd.
 Require Import DoubleSub.
@@ -21,7 +22,6 @@ Require Import DoubleSqrt.
 Require Import DoubleLift.
 Require Import DoubleDivn1.
 Require Import DoubleDiv.
-Require Import CyclicAxioms.
 
 Local Open Scope Z_scope.
 
diff --git a/CyclicDouble/DoubleDiv.v b/CyclicDouble/DoubleDiv.v
index 6bb78c6..1c441cd 100644
--- a/CyclicDouble/DoubleDiv.v
+++ b/CyclicDouble/DoubleDiv.v
@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 Require Import DoubleDivn1.
 Require Import DoubleAdd.
diff --git a/CyclicDouble/DoubleDivn1.v b/CyclicDouble/DoubleDivn1.v
index 9d0b354..f95a0b2 100644
--- a/CyclicDouble/DoubleDivn1.v
+++ b/CyclicDouble/DoubleDivn1.v
@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
diff --git a/CyclicDouble/DoubleLift.v b/CyclicDouble/DoubleLift.v
index 75a6571..f868c3b 100644
--- a/CyclicDouble/DoubleLift.v
+++ b/CyclicDouble/DoubleLift.v
@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
diff --git a/CyclicDouble/DoubleMul.v b/CyclicDouble/DoubleMul.v
index 8bcd050..d70f8e4 100644
--- a/CyclicDouble/DoubleMul.v
+++ b/CyclicDouble/DoubleMul.v
@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
diff --git a/CyclicDouble/DoubleSqrt.v b/CyclicDouble/DoubleSqrt.v
index 4943436..dc26397 100644
--- a/CyclicDouble/DoubleSqrt.v
+++ b/CyclicDouble/DoubleSqrt.v
@@ -10,9 +10,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
diff --git a/CyclicDouble/DoubleSub.v b/CyclicDouble/DoubleSub.v
index 8973b2b..e5136e3 100644
--- a/CyclicDouble/DoubleSub.v
+++ b/CyclicDouble/DoubleSub.v
@@ -11,9 +11,9 @@
 
 Set Implicit Arguments.
 
-Require Import ZArith Lia.
+From Stdlib Require Import ZArith Lia.
+From Stdlib Require Import DoubleType.
 Require Import BigNumPrelude.
-Require Import DoubleType.
 Require Import DoubleBase.
 
 Local Open Scope Z_scope.
diff --git a/SpecViaQ/QSig.v b/SpecViaQ/QSig.v
index 90cf7a0..d994090 100644
--- a/SpecViaQ/QSig.v
+++ b/SpecViaQ/QSig.v
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax.
+From Stdlib Require Import QArith Qpower Qminmax.
+From Stdlib Require Import Orders RelationPairs GenericMinMax.
 
 Open Scope Q_scope.
 
diff --git a/SpecViaZ/.lia.cache b/SpecViaZ/.lia.cache
index 988c28a..9589a40 100644
Binary files a/SpecViaZ/.lia.cache and b/SpecViaZ/.lia.cache differ
diff --git a/SpecViaZ/NSig.v b/SpecViaZ/NSig.v
index 8406ce4..8493f0b 100644
--- a/SpecViaZ/NSig.v
+++ b/SpecViaZ/NSig.v
@@ -8,7 +8,8 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import BinInt DoubleBase.
+From Stdlib Require Import BinInt.
+Require Import DoubleBase.
 
 Open Scope Z_scope.
 
diff --git a/SpecViaZ/NSigNAxioms.v b/SpecViaZ/NSigNAxioms.v
index 610d0f3..4d24b0b 100644
--- a/SpecViaZ/NSigNAxioms.v
+++ b/SpecViaZ/NSigNAxioms.v
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith OrdersFacts Nnat NAxioms NSig Lia.
+From Stdlib Require Import ZArith OrdersFacts Nnat NAxioms Lia.
+Require Import NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 
diff --git a/SpecViaZ/ZSig.v b/SpecViaZ/ZSig.v
index 80c1486..a2d1770 100644
--- a/SpecViaZ/ZSig.v
+++ b/SpecViaZ/ZSig.v
@@ -8,7 +8,8 @@
 (*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
 (************************************************************************)
 
-Require Import BinInt DoubleBase.
+From Stdlib Require Import BinInt.
+Require Import DoubleBase.
 
 Open Scope Z_scope.
 
diff --git a/SpecViaZ/ZSigZAxioms.v b/SpecViaZ/ZSigZAxioms.v
index abc2eae..97f50bd 100644
--- a/SpecViaZ/ZSigZAxioms.v
+++ b/SpecViaZ/ZSigZAxioms.v
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Bool ZArith OrdersFacts Nnat ZAxioms ZSig Lia.
+From Stdlib Require Import Bool ZArith OrdersFacts Nnat ZAxioms Lia.
+Require Import ZSig.
 
 (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
 
diff --git a/plugin/bignums_syntax.ml b/plugin/bignums_syntax.ml
index cd0cd32..a96448c 100644
--- a/plugin/bignums_syntax.ml
+++ b/plugin/bignums_syntax.ml
@@ -108,8 +108,8 @@ let word_of_pos_bigint ?loc hght n =
   decomp hght n
 
 let nat_of_int ?loc n =
-  let ref_O = DAst.make ?loc (GRef (Coqlib.lib_ref "num.nat.O", None)) in
-  let ref_S = DAst.make ?loc (GRef (Coqlib.lib_ref "num.nat.S", None)) in
+  let ref_O = DAst.make ?loc (GRef (Rocqlib.lib_ref "num.nat.O", None)) in
+  let ref_S = DAst.make ?loc (GRef (Rocqlib.lib_ref "num.nat.S", None)) in
   let rec mk_nat acc n =
     if Int.equal n 0 then acc
     else