From 823afcd4a1d354924a9389414fe4f2feee260056 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sun, 21 Jul 2024 14:13:29 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 algebra/CMonoids.v                   |  2 +-
 algebra/CRing_as_Ring.v              |  3 ++-
 algebra/CSums.v                      |  2 +-
 algebra/Expon.v                      |  2 +-
 complex/NRootCC.v                    |  4 ++--
 coq_reals/Rreals_iso.v               | 22 +++++++++++-----------
 fta/KeyLemma.v                       |  4 ++--
 ftc/WeakIVTQ.v                       |  2 +-
 logic/CLogic.v                       |  8 ++++----
 logic/CornBasics.v                   |  4 ++--
 metric2/Compact.v                    |  6 +++---
 metric2/Hausdorff.v                  |  2 +-
 metric2/Limit.v                      |  4 ++--
 metric2/Metric.v                     |  4 ++--
 model/Zmod/ZBasics.v                 |  2 +-
 model/Zmod/ZDivides.v                | 16 ++++++++--------
 model/metric2/L1metric.v             |  4 ++--
 model/metric2/LinfMetric.v           |  4 ++--
 model/metric2/LinfMetricMonad.v      |  4 ++--
 model/metric2/Qmetric.v              |  4 ++--
 model/setoids/Zfinsetoid.v           |  2 +-
 model/setoids/decsetoid.v            |  7 ++-----
 model/structures/NNUpperR.v          |  5 +++--
 model/structures/Nsec.v              |  4 ++--
 model/structures/OpenUnit.v          |  2 +-
 model/structures/Qinf.v              |  7 +++----
 model/structures/QnonNeg.v           |  6 ++++--
 model/structures/QposInf.v           |  2 +-
 model/structures/Qpossec.v           | 12 ++++++------
 model/structures/Qsec.v              |  6 +++---
 model/structures/StepQsec.v          |  6 +++---
 model/structures/Zsec.v              |  4 ++--
 model/totalorder/QMinMax.v           |  2 +-
 model/totalorder/QposMinMax.v        |  5 ++---
 model/totalorder/ZMinMax.v           |  6 +++---
 ode/AbstractIntegration.v            |  9 +++++----
 ode/BanachFixpoint.v                 |  8 ++++----
 ode/Picard.v                         |  9 +++++----
 ode/SimpleIntegration.v              | 12 ++++++------
 ode/metric.v                         |  8 ++++----
 raster/Raster.v                      |  2 +-
 reals/Max_AbsIR.v                    |  2 +-
 reals/Q_in_CReals.v                  |  2 +-
 reals/fast/CRAlternatingSum.v        |  6 +++---
 reals/fast/CRAlternatingSum_alg.v    |  8 ++++----
 reals/fast/CRArith.v                 | 12 ++++++------
 reals/fast/CRArith_alg.v             | 12 ++++++------
 reals/fast/CRFieldOps.v              |  2 +-
 reals/fast/CRGeometricSum.v          |  6 +++---
 reals/fast/CRabs.v                   |  2 +-
 reals/fast/CRarctan.v                |  2 +-
 reals/fast/CRarctan_small.v          |  2 +-
 reals/fast/CRartanh_slow.v           |  4 ++--
 reals/fast/CRball.v                  |  4 ++--
 reals/fast/CRcorrect.v               |  2 +-
 reals/fast/CRcos.v                   |  4 ++--
 reals/fast/CRexp.v                   |  6 +++---
 reals/fast/CRln.v                    |  2 +-
 reals/fast/CRpower.v                 |  4 ++--
 reals/fast/CRroot.v                  |  2 +-
 reals/fast/CRsin.v                   |  4 ++--
 reals/fast/CRstreams.v               | 11 ++++++-----
 reals/fast/Compress.v                |  2 +-
 reals/fast/Integration.v             |  4 ++--
 reals/fast/Interval.v                |  4 ++--
 reals/fast/MultivariatePolynomials.v |  2 +-
 reals/fast/Plot.v                    |  2 +-
 reals/fast/PowerBound.v              |  6 +++---
 reals/fast/RasterizeQ.v              |  4 ++--
 reals/fast/uneven_CRplus.v           |  4 ++--
 reals/faster/ACarith.v               |  5 ++---
 reals/faster/AQmetric.v              |  4 ++--
 reals/faster/ARAlternatingSum.v      |  5 ++---
 reals/faster/ARArith.v               |  5 ++---
 reals/faster/ARQ.v                   |  6 ++++--
 reals/faster/ARabs.v                 |  5 ++---
 reals/faster/ARbigD.v                |  4 ++--
 reals/faster/ARbigQ.v                |  4 ++--
 reals/faster/ARexp.v                 |  9 +++++----
 reals/faster/ARinterval.v            |  5 ++---
 reals/faster/ARplot.v                |  2 +-
 reals/faster/ARroot.v                |  8 +++++---
 reals/faster/ARsign.v                |  3 ++-
 reals/faster/ARsin.v                 |  5 ++---
 reals/faster/ApproximateRationals.v  |  9 +++++----
 reals/stdlib/CMTIntegrableSets.v     | 16 ++++++++--------
 reals/stdlib/ConstructiveFastReals.v |  4 ++--
 reals/stdlib/Markov.v                |  6 +++---
 stdlib_omissions/Q.v                 |  6 ++----
 stdlib_omissions/Z.v                 |  5 +++--
 tactics/Qauto.v                      |  4 ++--
 util/Extract.v                       |  1 +
 util/PointFree.v                     |  3 ++-
 util/Qdlog.v                         |  4 ++--
 util/Qgcd.v                          |  5 ++---
 util/Qsums.v                         | 13 ++++++-------
 96 files changed, 251 insertions(+), 249 deletions(-)

diff --git a/algebra/CMonoids.v b/algebra/CMonoids.v
index 740d34489..d2f89e4ef 100644
--- a/algebra/CMonoids.v
+++ b/algebra/CMonoids.v
@@ -36,7 +36,7 @@
 
 (** printing [0] %\ensuremath{\mathbf0}% #0# *)
 
-Require Export Coq.Arith.Euclid.
+From Coq Require Export Euclid.
 Require Export CoRN.model.Zmod.Cmod.
 Require Export CoRN.algebra.CSemiGroups.
 Require Export CoRN.tactics.csetoid_rewrite.
diff --git a/algebra/CRing_as_Ring.v b/algebra/CRing_as_Ring.v
index b612cd419..de634bfc4 100644
--- a/algebra/CRing_as_Ring.v
+++ b/algebra/CRing_as_Ring.v
@@ -1,5 +1,6 @@
 
-Require Export CoRN.algebra.CRings Coq.setoid_ring.Ring.
+Require Export CoRN.algebra.CRings.
+From Coq Require Export Ring.
 Definition CRing_Ring(R:CRing):(ring_theory (@cm_unit R) (@cr_one R) (@csg_op R) (@cr_mult R) (fun x y => x [-] y) (@cg_inv R) (@cs_eq R)).
 Proof.
  split;algebra.
diff --git a/algebra/CSums.v b/algebra/CSums.v
index d592ecfed..41d4b52d3 100644
--- a/algebra/CSums.v
+++ b/algebra/CSums.v
@@ -41,7 +41,7 @@
 (** printing Sumx %\ensuremath{\sum'}% #&sum;'&*)
 
 Require Export CoRN.algebra.CAbGroups.
-Require Export Coq.Arith.Peano_dec.
+From Coq Require Export Peano_dec.
 From Coq Require Import Lia.
 
 (**
diff --git a/algebra/Expon.v b/algebra/Expon.v
index ea3ca6f0a..0ba81e44a 100644
--- a/algebra/Expon.v
+++ b/algebra/Expon.v
@@ -36,7 +36,7 @@
 
 (** printing [^^] %\ensuremath{\hat{\ }}% #^# *)
 
-Require Export Coq.Arith.Arith.
+From Coq Require Export Arith.
 Require Export CoRN.algebra.COrdCauchy.
 From Coq Require Import Lia.
 
diff --git a/complex/NRootCC.v b/complex/NRootCC.v
index 6f3810265..a2644e808 100644
--- a/complex/NRootCC.v
+++ b/complex/NRootCC.v
@@ -40,8 +40,8 @@
 (** printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
 
 Require Export CoRN.complex.CComplex.
-Require Export Coq.Arith.Wf_nat.
-Require Export Coq.setoid_ring.ArithRing.
+From Coq Require Export Wf_nat.
+From Coq Require Export ArithRing.
 Import CRing_Homomorphisms.coercions.
 
 (**
diff --git a/coq_reals/Rreals_iso.v b/coq_reals/Rreals_iso.v
index 42cc3481b..473cb23ce 100644
--- a/coq_reals/Rreals_iso.v
+++ b/coq_reals/Rreals_iso.v
@@ -17,22 +17,22 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Import Coq.QArith.QArith.
-Require Import Coq.QArith.Qreals.
-Require Import Coq.QArith.QArith_base.
+From Coq Require Import QArith.
+From Coq Require Import Qreals.
+From Coq Require Import QArith_base.
 Require Import CoRN.tactics.CornTac.
-Require Import Coq.Reals.RIneq.
-Require Import Coq.Reals.Rcomplete.
-Require Import Coq.Reals.Rlimit.
-Require Import Coq.Reals.Rbasic_fun.
+From Coq Require Import RIneq.
+From Coq Require Import Rcomplete.
+From Coq Require Import Rlimit.
+From Coq Require Import Rbasic_fun.
 Require Import CoRN.coq_reals.Rreals.
 Require Import CoRN.reals.iso_CReals.
 Require Import CoRN.reals.CauchySeq.
-Require Import Coq.Reals.Rtrigo_def.
+From Coq Require Import Rtrigo_def.
 Require Import CoRN.transc.PowerSeries.
-Require Import Coq.Logic.ConstructiveEpsilon.
-Require Import Coq.Reals.Rlogic.
-Require Export Coq.Reals.Reals.
+From Coq Require Import ConstructiveEpsilon.
+From Coq Require Import Rlogic.
+From Coq Require Export Reals.
 Require Import CoRN.transc.Pi.
 Require Import CoRN.transc.MoreArcTan.
 Require Import CoRN.logic.PropDecid.
diff --git a/fta/KeyLemma.v b/fta/KeyLemma.v
index 2b4bde0ef..5c17a1994 100644
--- a/fta/KeyLemma.v
+++ b/fta/KeyLemma.v
@@ -34,8 +34,8 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-Require Export Coq.ZArith.ZArith.
-Require Export Coq.Arith.Compare.
+From Coq Require Export ZArith.
+From Coq Require Export Compare.
 Require Export CoRN.reals.NRootIR.
 From Coq Require Import Lia.
 
diff --git a/ftc/WeakIVTQ.v b/ftc/WeakIVTQ.v
index 261d82439..37a5f9701 100644
--- a/ftc/WeakIVTQ.v
+++ b/ftc/WeakIVTQ.v
@@ -7,7 +7,7 @@ Definition Q2R  (q: Q) : IR := (inj_Q IR q).
 Coercion  Q2R : Q >-> st_car.
 
 
-Require Import Coq.setoid_ring.Ring. 
+From Coq Require Import Ring.
 Require Import CoRN.tactics.CornTac.
 Require Import CoRN.algebra.CRing_as_Ring.
 
diff --git a/logic/CLogic.v b/logic/CLogic.v
index 00ace5225..168472a68 100644
--- a/logic/CLogic.v
+++ b/logic/CLogic.v
@@ -44,11 +44,11 @@
 (** printing or %\ensuremath{\mathrel\vee}% *)
 (** printing and %\ensuremath{\mathrel\wedge}% *)
 
-Require Export Coq.Arith.Compare_dec.
+From Coq Require Export Compare_dec.
 Require Export CoRN.logic.CornBasics.
-Require Export Coq.ZArith.ZArith.
-Require Export Coq.setoid_ring.ZArithRing.
-Require Export Coq.Arith.Wf_nat.
+From Coq Require Export ZArith.
+From Coq Require Export ZArithRing.
+From Coq Require Export Wf_nat.
 From Coq Require Import Lia.
 
 
diff --git a/logic/CornBasics.v b/logic/CornBasics.v
index 8ef30b0c5..75bfc5563 100644
--- a/logic/CornBasics.v
+++ b/logic/CornBasics.v
@@ -48,8 +48,8 @@
 From Coq Require Export ZArith.
 From Coq Require Import Lia.
 Require Export CoRN.stdlib_omissions.List.
-Require Import Coq.Logic.Eqdep_dec.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import Eqdep_dec.
+From Coq Require Import Setoid.
 
 Tactic Notation "apply" ":" constr(x) := pose proof x as HHH; first [
   refine HHH | 
diff --git a/metric2/Compact.v b/metric2/Compact.v
index c0a32f534..dc6f3f6a4 100644
--- a/metric2/Compact.v
+++ b/metric2/Compact.v
@@ -21,11 +21,11 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 Require Import CoRN.model.totalorder.QposMinMax.
 Require Import CoRN.metric2.Limit.
 Require Export CoRN.metric2.FinEnum.
-Require Import Coq.ZArith.Zpow_facts.
+From Coq Require Import Zpow_facts.
 Require Export CoRN.metric2.Complete.
 Require Import CoRN.logic.Classic.
-Require Import Coq.QArith.Qpower.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qpower.
+From Coq Require Import Qround.
 
 Set Implicit Arguments.
 
diff --git a/metric2/Hausdorff.v b/metric2/Hausdorff.v
index 3926fa1bb..2616126ac 100644
--- a/metric2/Hausdorff.v
+++ b/metric2/Hausdorff.v
@@ -23,7 +23,7 @@ Require Import CoRN.logic.Classic.
 Require Export CoRN.metric2.Metric.
 Require Import CoRN.metric2.Classification.
 Require Import Coq.Lists.List.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.model.totalorder.QposMinMax.
 
diff --git a/metric2/Limit.v b/metric2/Limit.v
index cb8c97c0a..8d23bafcd 100644
--- a/metric2/Limit.v
+++ b/metric2/Limit.v
@@ -21,8 +21,8 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.QArith.QArith.
-Require Import Coq.Bool.Bool.
+From Coq Require Import QArith.
+From Coq Require Import Bool.
 Require Export CoRN.metric2.Complete.
 Require Export MathClasses.theory.CoqStreams.
 Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals.
diff --git a/metric2/Metric.v b/metric2/Metric.v
index 1d9a03136..aab9c848a 100644
--- a/metric2/Metric.v
+++ b/metric2/Metric.v
@@ -20,8 +20,8 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Export Coq.QArith.QArith.
-Require Import CoRN.algebra.RSetoid. 
+From Coq Require Export QArith.
+Require Import CoRN.algebra.RSetoid.
 Require Import MathClasses.interfaces.canonical_names.
 Require Import MathClasses.interfaces.abstract_algebra.
 
diff --git a/model/Zmod/ZBasics.v b/model/Zmod/ZBasics.v
index 399c93d2b..9cbdf08b7 100644
--- a/model/Zmod/ZBasics.v
+++ b/model/Zmod/ZBasics.v
@@ -35,7 +35,7 @@
  *)
 (* ZBasics.v, by Vince Barany *)
 
-Require Export Coq.ZArith.ZArith.
+From Coq Require Export ZArith.
 Require Export CoRN.logic.CLogic.
 From Coq Require Import Lia.
 
diff --git a/model/Zmod/ZDivides.v b/model/Zmod/ZDivides.v
index d356a926c..9fba7e10f 100644
--- a/model/Zmod/ZDivides.v
+++ b/model/Zmod/ZDivides.v
@@ -503,10 +503,10 @@ Proof.
   case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
     auto with zarith.
    intros p q.
-   elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
+   elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
    intros Hlt Hp HR; rewrite HR; auto with zarith.
   intros p q.
-  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
+  elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
   case R.
     auto with zarith.
    intro r'; intros H0 H1 H2.
@@ -518,10 +518,10 @@ Proof.
  case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
    auto with zarith.
   intros p q.
-  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
+  elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
   case R; intros r' H0; intros; try (cut (Zpos r' = Zpos p); elim H0); auto with zarith.
  intros p q.
- elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
+ elim (BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
  case R; intros; try discriminate; try tauto.
 Qed.
 
@@ -536,12 +536,12 @@ Proof.
   case b; unfold Z.opp in |- *.
     auto.
    intro B.
-   elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
+   elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
    intro Hr; rewrite Hr; auto.
   intro B.
   generalize (Z_mod_lt (Zpos A) (Zpos B)).
   unfold Z.modulo, Z.div_eucl in |- *.
-  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
+  elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
   case r.
     intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
    intros R Hlt HR.
@@ -558,7 +558,7 @@ Proof.
   intro B.
   generalize (Z_mod_lt (Zpos A) (Zpos B)).
   unfold Z.modulo, Z.div_eucl in |- *.
-  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
+  elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
   case r.
     intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
    intros R Hlt HR.
@@ -572,7 +572,7 @@ Proof.
  intro B.
  generalize (Z_mod_lt (Zpos A) (Zpos B)).
  unfold Z.modulo, Z.div_eucl in |- *.
- elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
+ elim (BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
  case r.
    intros _ HR; fold (- q)%Z in |- *; auto.
   intros; discriminate.
diff --git a/model/metric2/L1metric.v b/model/metric2/L1metric.v
index bfa9f77d7..87c1aae4f 100644
--- a/model/metric2/L1metric.v
+++ b/model/metric2/L1metric.v
@@ -26,9 +26,9 @@ Require Export CoRN.model.structures.StepQsec.
 Require Export CoRN.metric2.UniformContinuity.
 Require Import CoRN.metric2.Prelength.
 Require Import CoRN.model.structures.OpenUnit.
-Require Import Coq.QArith.QArith.
+From Coq Require Import QArith.
 Require Import CoRN.model.totalorder.QMinMax.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.algebra.COrdFields2.
diff --git a/model/metric2/LinfMetric.v b/model/metric2/LinfMetric.v
index 277f9c359..002997c28 100644
--- a/model/metric2/LinfMetric.v
+++ b/model/metric2/LinfMetric.v
@@ -27,9 +27,9 @@ Require Import CoRN.metric2.Prelength.
 Require Import CoRN.model.metric2.L1metric.
 Require Export CoRN.model.metric2.LinfMetricMonad.
 Require Import CoRN.model.structures.OpenUnit.
-Require Import Coq.QArith.QArith.
+From Coq Require Import QArith.
 Require Import CoRN.model.totalorder.QMinMax.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.algebra.COrdFields2.
diff --git a/model/metric2/LinfMetricMonad.v b/model/metric2/LinfMetricMonad.v
index 01b270095..4f4797900 100644
--- a/model/metric2/LinfMetricMonad.v
+++ b/model/metric2/LinfMetricMonad.v
@@ -29,9 +29,9 @@ Require Export CoRN.metric2.StepFunctionSetoid.
 Require Import CoRN.metric2.StepFunctionMonad.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.structures.OpenUnit.
-Require Import Coq.QArith.QArith.
+From Coq Require Import QArith.
 Require Import CoRN.model.totalorder.QMinMax.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.metric2.Prelength.
diff --git a/model/metric2/Qmetric.v b/model/metric2/Qmetric.v
index 61c5ed5e0..6acaac6b7 100644
--- a/model/metric2/Qmetric.v
+++ b/model/metric2/Qmetric.v
@@ -24,7 +24,7 @@ Require Import CoRN.metric2.Prelength.
 Require Import CoRN.metric2.Classification.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import MathClasses.implementations.stdlib_rationals.
 
@@ -444,7 +444,7 @@ Proof with auto.
  apply ball_sym...
 Qed.
 
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qround.
 
 Lemma Qfloor_ball q:
   Qball (1#2) ((Qfloor q # 1) + (1#2)) q.
diff --git a/model/setoids/Zfinsetoid.v b/model/setoids/Zfinsetoid.v
index 344985b6b..6620e0ad9 100644
--- a/model/setoids/Zfinsetoid.v
+++ b/model/setoids/Zfinsetoid.v
@@ -33,7 +33,7 @@
  * with this work; if not, write to the Free Software Foundation, Inc.,
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
-Require Export Coq.ZArith.ZArith.
+From Coq Require Export ZArith.
 Require Import CoRN.algebra.CSetoids.
 
 (**
diff --git a/model/setoids/decsetoid.v b/model/setoids/decsetoid.v
index fa6dc5a58..b2e6812da 100644
--- a/model/setoids/decsetoid.v
+++ b/model/setoids/decsetoid.v
@@ -4,11 +4,8 @@
 
 Set Implicit Arguments.
 
-Require Import
- CoRN.algebra.CSetoids
- Coq.Classes.SetoidDec
- Coq.Classes.Morphisms
- Coq.Classes.SetoidClass.
+Require Import CoRN.algebra.CSetoids.
+From Coq Require Import SetoidDec Morphisms SetoidClass.
 
 
 Class Apartness `{SetoidClass.Setoid} (ap: Crelation A): Type :=
diff --git a/model/structures/NNUpperR.v b/model/structures/NNUpperR.v
index 72ef10ea5..7d02934a7 100644
--- a/model/structures/NNUpperR.v
+++ b/model/structures/NNUpperR.v
@@ -1,7 +1,8 @@
 (* This module is designed to *not* be Import'ed, only Require'd. *)
 
-Require Import
-  Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program.
+From Coq Require Import Qabs.
+Require Import CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec.
+From Coq Require Import Qminmax Ring Program.
 
 Require CoRN.model.structures.QnonNeg.
 Import QnonNeg.notations QnonNeg.coercions.
diff --git a/model/structures/Nsec.v b/model/structures/Nsec.v
index 0b27fae03..24994f1e7 100644
--- a/model/structures/Nsec.v
+++ b/model/structures/Nsec.v
@@ -36,8 +36,8 @@
 
 (** printing {#N} $\ensuremath{\mathrel\#_{\mathbb N}}$ *)
 
-Require Export Coq.Arith.Peano_dec.
-Require Export Coq.Relations.Relations.
+From Coq Require Export Peano_dec.
+From Coq Require Export Relations.
 Require Import CoRN.logic.CLogic.
 From Coq Require Import Lia.
 
diff --git a/model/structures/OpenUnit.v b/model/structures/OpenUnit.v
index 6028831a3..d81b1fd55 100644
--- a/model/structures/OpenUnit.v
+++ b/model/structures/OpenUnit.v
@@ -18,7 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
 IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
-Require Export Coq.QArith.QArith.
+From Coq Require Export QArith.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.algebra.COrdFields.
 Require Import CoRN.tactics.Qauto.
diff --git a/model/structures/Qinf.v b/model/structures/Qinf.v
index 3a2fea274..5761eefa2 100644
--- a/model/structures/Qinf.v
+++ b/model/structures/Qinf.v
@@ -1,7 +1,6 @@
-Require Import
- CoRN.model.totalorder.QposMinMax
- Coq.Setoids.Setoid Coq.Arith.Arith
- CoRN.model.rings.Qring CoRN.model.structures.QposInf
+Require Import CoRN.model.totalorder.QposMinMax.
+From Coq Require Import Setoid Arith.
+Require Import CoRN.model.rings.Qring CoRN.model.structures.QposInf
  CoRN.stdlib_omissions.Q
  MathClasses.interfaces.abstract_algebra
  MathClasses.implementations.stdlib_rationals
diff --git a/model/structures/QnonNeg.v b/model/structures/QnonNeg.v
index f9471a157..128d4ae6f 100644
--- a/model/structures/QnonNeg.v
+++ b/model/structures/QnonNeg.v
@@ -1,7 +1,9 @@
 (* This module is designed to *not* be Import'ed, only Require'd. *)
 
-Require Import CoRN.model.totalorder.QposMinMax 
-        Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax.
+Require Import CoRN.model.totalorder.QposMinMax.
+From Coq Require Import Program.
+Require Import CoRN.model.structures.QposInf.
+From Coq Require Import Qminmax.
 
 
 (* The data type and simple relations/constants: *)
diff --git a/model/structures/QposInf.v b/model/structures/QposInf.v
index 34350e812..4d766bb44 100644
--- a/model/structures/QposInf.v
+++ b/model/structures/QposInf.v
@@ -19,7 +19,7 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Export Coq.QArith.QArith.
+From Coq Require Export QArith.
 Require Import CoRN.model.totalorder.QposMinMax.
 
 (** printing QposInf $\mathbb{Q}^{+}_{\infty}$ #Q<SUP>+</SUP><SUB>&infin;</SUB># *)
diff --git a/model/structures/Qpossec.v b/model/structures/Qpossec.v
index 97946a507..544b6ef6f 100644
--- a/model/structures/Qpossec.v
+++ b/model/structures/Qpossec.v
@@ -36,14 +36,14 @@
 
 (** printing Qpos $\mathbb{Q}^{+}$ #Q<SUP>+</SUP># *)
 
-Require Export Coq.QArith.QArith.
-Require Import Coq.QArith.Qpower.
+From Coq Require Export QArith.
+From Coq Require Import Qpower.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.algebra.COrdFields2.
-Require Import Coq.Logic.Eqdep_dec.
+From Coq Require Import Eqdep_dec.
 Require Import CoRN.tactics.CornTac.
-Require Import Coq.QArith.Qround.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qround.
+From Coq Require Import Qabs.
 Require Import CoRN.stdlib_omissions.Q.
 
 (* Backwards compatibility for Hint Rewrite locality attributes *)
@@ -137,7 +137,7 @@ Lemma positive_Z (z: Z): Z.lt 0 z -> sig (fun p: positive => Zpos p = z).
 Defined.
 
 (* todo: move this Qlt_uniq stuff elsewhere *)
-Require Coq.Logic.Eqdep_dec.
+From Coq Require Eqdep_dec.
 
 Definition comparison_eq_dec (a b: comparison): { a = b } + { a <> b}.
  destruct a, b; try (left; reflexivity); try (right; discriminate).
diff --git a/model/structures/Qsec.v b/model/structures/Qsec.v
index faee68706..149af4cd9 100644
--- a/model/structures/Qsec.v
+++ b/model/structures/Qsec.v
@@ -41,10 +41,10 @@
 (** printing QFOUR %\ensuremath{4_\mathbb{Q}}% #4<sub>Q</sub># *)
 
 Require Export CoRN.logic.CLogic.
-Require Import Coq.Arith.Arith.
-Require Import Coq.Arith.Peano_dec.
+From Coq Require Import Arith.
+From Coq Require Import Peano_dec.
 Require Import CoRN.model.structures.Zsec.
-Require Export Coq.QArith.QArith.
+From Coq Require Export QArith.
 Require Import CoRN.stdlib_omissions.Q.
 
 Close Scope Q_scope.
diff --git a/model/structures/StepQsec.v b/model/structures/StepQsec.v
index cc03aee19..a2e40ab4e 100644
--- a/model/structures/StepQsec.v
+++ b/model/structures/StepQsec.v
@@ -1,9 +1,9 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.model.metric2.Qmetric.
-Require Export Coq.QArith.QArith.
+From Coq Require Export QArith.
 Require Export CoRN.metric2.StepFunctionSetoid.
-Require Import Coq.QArith.Qabs.
-Require Import Coq.Bool.Bool.
+From Coq Require Import Qabs.
+From Coq Require Import Bool.
 Require Import CoRN.tactics.CornTac.
 Require Import CoRN.logic.CornBasics.
 Require Import CoRN.algebra.RSetoid.
diff --git a/model/structures/Zsec.v b/model/structures/Zsec.v
index 7168ef977..2db818e4b 100644
--- a/model/structures/Zsec.v
+++ b/model/structures/Zsec.v
@@ -36,9 +36,9 @@
 
 (** printing {#Z} %\ensuremath{\mathrel\#_{\mathbb Z}}% *)
 
-Require Export Coq.ZArith.ZArith.
+From Coq Require Export ZArith.
 Require Import CoRN.logic.CLogic.
-Require Import Coq.Setoids.Setoid.
+From Coq Require Import Setoid.
 
 #[global]
 Instance Z_default : @DefaultRelation Z (@eq Z) | 2 := {}.
diff --git a/model/totalorder/QMinMax.v b/model/totalorder/QMinMax.v
index bb3b2df4b..c868d6ee2 100644
--- a/model/totalorder/QMinMax.v
+++ b/model/totalorder/QMinMax.v
@@ -19,7 +19,7 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Import Coq.QArith.QArith_base.
+From Coq Require Import QArith_base.
 Require Import CoRN.order.TotalOrder.
 
 (**
diff --git a/model/totalorder/QposMinMax.v b/model/totalorder/QposMinMax.v
index 82ff8e0ee..cf4ec717a 100644
--- a/model/totalorder/QposMinMax.v
+++ b/model/totalorder/QposMinMax.v
@@ -19,9 +19,8 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Import Coq.Logic.Eqdep_dec.
-Require Import Coq.QArith.QArith Coq.QArith.Qabs.
-Require Import Coq.QArith.Qpower Coq.QArith.Qround.
+From Coq Require Import Eqdep_dec.
+From Coq Require Import QArith Qabs Qpower Qround.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.order.TotalOrder.
 
diff --git a/model/totalorder/ZMinMax.v b/model/totalorder/ZMinMax.v
index a1d05eea1..9355194be 100644
--- a/model/totalorder/ZMinMax.v
+++ b/model/totalorder/ZMinMax.v
@@ -19,9 +19,9 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Export Coq.ZArith.Zmin.
-Require Export Coq.ZArith.Zmax.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Export Zmin.
+From Coq Require Export Zmax.
+From Coq Require Import ZArith.
 Require Import CoRN.order.TotalOrder.
 
 Opaque Z_lt_le_dec.
diff --git a/ode/AbstractIntegration.v b/ode/AbstractIntegration.v
index dd93194ba..117663781 100644
--- a/ode/AbstractIntegration.v
+++ b/ode/AbstractIntegration.v
@@ -5,10 +5,11 @@ Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.reals.CRreal.
-Require Import
- Coq.Unicode.Utf8 Coq.Program.Program
- CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs
- CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric
+From Coq Require Import Utf8 Program.
+Require Import CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs
+ CoRN.tactics.Qauto.
+From Coq Require Import Qround.
+Require Import CoRN.model.metric2.Qmetric
  CoRN.stdlib_omissions.P
  CoRN.stdlib_omissions.Z
  CoRN.stdlib_omissions.Q
diff --git a/ode/BanachFixpoint.v b/ode/BanachFixpoint.v
index 18169051f..19594b319 100644
--- a/ode/BanachFixpoint.v
+++ b/ode/BanachFixpoint.v
@@ -1,10 +1,10 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.QArith.QArith
-  MathClasses.implementations.stdlib_rationals CoRN.model.structures.Qinf CoRN.model.structures.Qpossec CoRN.model.structures.QposInf CoRN.model.structures.QnonNeg MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations.
-Require Import CoRN.tactics.Qauto Coq.QArith.QOrderedType.
+From Coq Require Import QArith.
+Require Import MathClasses.implementations.stdlib_rationals CoRN.model.structures.Qinf CoRN.model.structures.Qpossec CoRN.model.structures.QposInf CoRN.model.structures.QnonNeg MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations.
+Require Import CoRN.tactics.Qauto.
+From Coq Require Import QOrderedType.
 Require Import MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow.
 Require Import MathClasses.interfaces.naturals MathClasses.interfaces.orders.
 Import peano_naturals.
diff --git a/ode/Picard.v b/ode/Picard.v
index a9e4c597c..2083624ba 100644
--- a/ode/Picard.v
+++ b/ode/Picard.v
@@ -2,10 +2,11 @@ Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.reals.CRreal.
-Require Import
- Coq.Unicode.Utf8 Coq.Program.Program
- CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs
- CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric
+From Coq Require Import Utf8 Program.
+Require Import CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs
+ CoRN.tactics.Qauto.
+From Coq Require Import Qround.
+Require Import CoRN.model.metric2.Qmetric
  (*stdlib_omissions.P
  stdlib_omissions.Z
  stdlib_omissions.Q
diff --git a/ode/SimpleIntegration.v b/ode/SimpleIntegration.v
index 8bff113b2..ce2002735 100644
--- a/ode/SimpleIntegration.v
+++ b/ode/SimpleIntegration.v
@@ -10,15 +10,15 @@ Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.reals.CRreal.
 Require Import
-  CoRN.stdlib_omissions.List Coq.Unicode.Utf8
-  Coq.QArith.QArith Coq.QArith.Qabs
-  CoRN.model.totalorder.QposMinMax CoRN.util.Qsums
+  CoRN.stdlib_omissions.List.
+From Coq Require Import Utf8 QArith Qabs.
+Require Import CoRN.model.totalorder.QposMinMax CoRN.util.Qsums
   CoRN.model.metric2.Qmetric CoRN.model.setoids.Qsetoid (* Needs imported for Q_is_Setoid to be a canonical structure *)
   CoRN.reals.fast.CRArith (*AbstractIntegration*)
   QnonNeg
-  CoRN.util.Qgcd
-  Coq.Program.Program
-  CoRN.reals.fast.uneven_CRplus
+  CoRN.util.Qgcd.
+From Coq Require Import Program.
+Require Import CoRN.reals.fast.uneven_CRplus
   CoRN.stdlib_omissions.P
   CoRN.stdlib_omissions.Z
   CoRN.stdlib_omissions.Q
diff --git a/ode/metric.v b/ode/metric.v
index 3c122e3b4..7c418b0f1 100644
--- a/ode/metric.v
+++ b/ode/metric.v
@@ -1,13 +1,13 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.QArith.QArith
-  MathClasses.theory.setoids (* Equiv Prop *) MathClasses.theory.products
+From Coq Require Import QArith.
+Require Import MathClasses.theory.setoids (* Equiv Prop *) MathClasses.theory.products
   MathClasses.implementations.stdlib_rationals (*Qinf*) (*Qpossec QposInf QnonNeg*) MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations.
 Require CoRN.model.structures.Qinf.
 (*Import (*QnonNeg.notations*) QArith.*)
-Require Import CoRN.tactics.Qauto Coq.QArith.QOrderedType.
+Require Import CoRN.tactics.Qauto.
+From Coq Require Import QOrderedType.
 (*Require Import orders.*)
 Require Import MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow.
 Require Import MathClasses.interfaces.naturals MathClasses.interfaces.orders.
diff --git a/raster/Raster.v b/raster/Raster.v
index 0c512e69a..154d36056 100644
--- a/raster/Raster.v
+++ b/raster/Raster.v
@@ -1,7 +1,7 @@
 Require Coq.Vectors.Vector.
 Export Vector.VectorNotations.
 Require Export CoRN.stdlib_omissions.List.
-Require Import Coq.Arith.Arith Coq.PArith.BinPos.
+From Coq Require Import Arith BinPos.
 
 Set Implicit Arguments.
 
diff --git a/reals/Max_AbsIR.v b/reals/Max_AbsIR.v
index be7232ae6..1b4609fd0 100644
--- a/reals/Max_AbsIR.v
+++ b/reals/Max_AbsIR.v
@@ -38,7 +38,7 @@
 (** printing Min %\ensuremath{\min}% *)
 
 Require Export CoRN.reals.Q_in_CReals.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Export CoRN.reals.CauchySeq.
 
 Section Maximum.
diff --git a/reals/Q_in_CReals.v b/reals/Q_in_CReals.v
index f17bf8b39..68142d5c6 100644
--- a/reals/Q_in_CReals.v
+++ b/reals/Q_in_CReals.v
@@ -48,7 +48,7 @@ Require Export CoRN.model.monoids.Nmonoid.
 Require Export CoRN.model.rings.Zring.
 Require Import CoRN.algebra.CRing_Homomorphisms.
 Require Import CoRN.algebra.Expon.
-Require Import Coq.QArith.Qpower.
+From Coq Require Import Qpower.
 Require Import CoRN.tactics.CornTac.
 
 Section Rational_sequence_prelogue.
diff --git a/reals/fast/CRAlternatingSum.v b/reals/fast/CRAlternatingSum.v
index e3e0d4552..1ed62b516 100644
--- a/reals/fast/CRAlternatingSum.v
+++ b/reals/fast/CRAlternatingSum.v
@@ -19,9 +19,9 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
 
-Require Import Coq.setoid_ring.ArithRing.
-Require Import Coq.Bool.Bool.
-Require Import Coq.QArith.Qpower Coq.QArith.Qabs.
+From Coq Require Import ArithRing.
+From Coq Require Import Bool.
+From Coq Require Import Qpower Qabs.
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
diff --git a/reals/fast/CRAlternatingSum_alg.v b/reals/fast/CRAlternatingSum_alg.v
index 098053a5c..43ee818e9 100644
--- a/reals/fast/CRAlternatingSum_alg.v
+++ b/reals/fast/CRAlternatingSum_alg.v
@@ -24,19 +24,19 @@ Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.reals.iso_CReals.
 Require Import CoRN.reals.Q_in_CReals.
-Require Import Coq.setoid_ring.ArithRing.
+From Coq Require Import ArithRing.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRIR.
 Require Import CoRN.reals.fast.CRabs.
-Require Import Coq.Bool.Bool.
+From Coq Require Import Bool.
 Require Import CoRN.algebra.COrdAbs.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Export CoRN.model.metric2.Qmetric.
 Require Import CoRN.reals.fast.LazyNat.
 Require Export CoRN.metric2.Limit.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.QArith.Qpower.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qpower.
+From Coq Require Import Qabs.
 Require Export MathClasses.theory.CoqStreams.
 Require Import CoRN.transc.PowerSeries.
 Require Import CoRN.tactics.CornTac.
diff --git a/reals/fast/CRArith.v b/reals/fast/CRArith.v
index 48a910711..caf9ec31f 100644
--- a/reals/fast/CRArith.v
+++ b/reals/fast/CRArith.v
@@ -24,17 +24,17 @@ Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.setoid_ring.Ring_theory.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.QArith.QArith.
-Require Import Coq.QArith.Qabs.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Ring_theory.
+From Coq Require Import Setoid.
+From Coq Require Import QArith.
+From Coq Require Import Qabs.
+From Coq Require Import Qround.
 Require Import CoRN.metric2.Complete.
 Require Import CoRN.metric2.ProductMetric.
 Require Export CoRN.reals.fast.CRFieldOps.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.logic.Stability.
-Require Import Coq.Logic.ConstructiveEpsilon.
+From Coq Require Import ConstructiveEpsilon.
 Require Import CoRN.util.Qdlog.
 Require Import MathClasses.interfaces.abstract_algebra.
 Require Import MathClasses.interfaces.orders.
diff --git a/reals/fast/CRArith_alg.v b/reals/fast/CRArith_alg.v
index 7f82aaff5..e9a990da5 100644
--- a/reals/fast/CRArith_alg.v
+++ b/reals/fast/CRArith_alg.v
@@ -23,11 +23,11 @@ Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.setoid_ring.Ring_theory.
-Require Import Coq.Setoids.Setoid.
-Require Import Coq.QArith.QArith.
-Require Import Coq.QArith.Qabs.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Ring_theory.
+From Coq Require Import Setoid.
+From Coq Require Import QArith.
+From Coq Require Import Qabs.
+From Coq Require Import Qround.
 Require Export CoRN.model.reals.CRreal.
 Require Import CoRN.metric2.Complete.
 Require Export CoRN.reals.fast.CRFieldOps.
@@ -36,7 +36,7 @@ Require Import CoRN.algebra.CRing_Homomorphisms.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.tactics.CornTac.
 Require Import CoRN.logic.Stability.
-Require Import Coq.Logic.ConstructiveEpsilon.
+From Coq Require Import ConstructiveEpsilon.
 Require Import CoRN.util.Qdlog.
 Require Import MathClasses.interfaces.abstract_algebra.
 Require Import MathClasses.interfaces.orders.
diff --git a/reals/fast/CRFieldOps.v b/reals/fast/CRFieldOps.v
index 9f03b52f9..9360b6947 100644
--- a/reals/fast/CRFieldOps.v
+++ b/reals/fast/CRFieldOps.v
@@ -25,7 +25,7 @@ Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.totalorder.QposMinMax.
 Require Export CoRN.model.lattice.CRlattice.
 Require Import CoRN.model.totalorder.QMinMax.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.metric2.ProductMetric.
 Require Import MathClasses.interfaces.canonical_names.
diff --git a/reals/fast/CRGeometricSum.v b/reals/fast/CRGeometricSum.v
index 2c6aafe79..df5120038 100644
--- a/reals/fast/CRGeometricSum.v
+++ b/reals/fast/CRGeometricSum.v
@@ -24,9 +24,9 @@ Require Import CoRN.reals.fast.CRAlternatingSum.
 Require Import CoRN.reals.fast.CRstreams.
 Require Import CoRN.model.totalorder.QposMinMax.
 Require Import CoRN.model.totalorder.QMinMax.
-Require Import Coq.QArith.Qpower.
-Require Import Coq.QArith.Qabs.
-Require Import Coq.ZArith.Zdiv.
+From Coq Require Import Qpower.
+From Coq Require Import Qabs.
+From Coq Require Import Zdiv.
 
 Set Implicit Arguments.
 
diff --git a/reals/fast/CRabs.v b/reals/fast/CRabs.v
index c0014f5a4..dc1acd6c9 100644
--- a/reals/fast/CRabs.v
+++ b/reals/fast/CRabs.v
@@ -25,7 +25,7 @@ Require Import CoRN.metric2.UniformContinuity.
 Require Export CoRN.model.totalorder.QposMinMax.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.model.metric2.Qmetric.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.logic.Stability.
 
diff --git a/reals/fast/CRarctan.v b/reals/fast/CRarctan.v
index cc2c63b63..c7220cb4d 100644
--- a/reals/fast/CRarctan.v
+++ b/reals/fast/CRarctan.v
@@ -34,7 +34,7 @@ Require Import CoRN.reals.fast.ContinuousCorrect.
 Require Import CoRN.tactics.CornTac.
 Require Import CoRN.stdlib_omissions.Q.
 Require Import MathClasses.interfaces.abstract_algebra.
-Require Import Coq.micromega.Psatz.
+From Coq Require Import Psatz.
 
 (* Backwards compatibility for Hint Rewrite locality attributes *)
 Set Warnings "-unsupported-attributes".
diff --git a/reals/fast/CRarctan_small.v b/reals/fast/CRarctan_small.v
index 6effa9515..1cbd1a9b6 100644
--- a/reals/fast/CRarctan_small.v
+++ b/reals/fast/CRarctan_small.v
@@ -28,7 +28,7 @@ Require Import CoRN.reals.fast.CRstreams.
 Require Import CoRN.reals.fast.CRexp.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRIR.
-Require Import Coq.QArith.Qpower Coq.QArith.Qabs Coq.QArith.Qround.
+From Coq Require Import Qpower Qabs Qround.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.reals.Q_in_CReals.
 Require Import CoRN.model.metric2.Qmetric.
diff --git a/reals/fast/CRartanh_slow.v b/reals/fast/CRartanh_slow.v
index 44a4eab8d..6c3fe8ff4 100644
--- a/reals/fast/CRartanh_slow.v
+++ b/reals/fast/CRartanh_slow.v
@@ -28,8 +28,8 @@ Require Import CoRN.reals.fast.CRGeometricSum.
 Require Import CoRN.reals.fast.CRstreams.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRIR.
-Require Import Coq.QArith.Qabs.
-Require Import Coq.QArith.Qpower.
+From Coq Require Import Qabs.
+From Coq Require Import Qpower.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.reals.Q_in_CReals.
 Require Import CoRN.model.metric2.Qmetric.
diff --git a/reals/fast/CRball.v b/reals/fast/CRball.v
index e0c4cb8a7..594a09bca 100644
--- a/reals/fast/CRball.v
+++ b/reals/fast/CRball.v
@@ -1,8 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
- Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs.
+From Coq Require Import Qabs.
+Require Import CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs.
 
 (** Balls with real radii instead of rational radii. *)
 
diff --git a/reals/fast/CRcorrect.v b/reals/fast/CRcorrect.v
index 2e5bab7c4..ae050ce8f 100644
--- a/reals/fast/CRcorrect.v
+++ b/reals/fast/CRcorrect.v
@@ -28,7 +28,7 @@ Require Import CoRN.tactics.CornTac.
 From Coq Require Import Lia.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.model.totalorder.QMinMax.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Export CoRN.reals.fast.CRFieldOps.
 
 (* Backwards compatibility for Hint Rewrite locality attributes *)
diff --git a/reals/fast/CRcos.v b/reals/fast/CRcos.v
index 66c4e3f8d..828aa3697 100644
--- a/reals/fast/CRcos.v
+++ b/reals/fast/CRcos.v
@@ -27,9 +27,9 @@ Require Import CoRN.reals.fast.CRsin.
 Require Import CoRN.reals.fast.CRpi.
 Require Import CoRN.reals.fast.CRIR.
 Require Import CoRN.reals.fast.Compress.
-Require Import Coq.QArith.Qpower.
+From Coq Require Import Qpower.
 Require Import CoRN.model.ordfields.Qordfield.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qround.
 Require Import CoRN.transc.Pi.
 Require Import CoRN.reals.fast.ModulusDerivative.
 Require Import CoRN.reals.fast.ContinuousCorrect.
diff --git a/reals/fast/CRexp.v b/reals/fast/CRexp.v
index 89936c3e2..4ac29b515 100644
--- a/reals/fast/CRexp.v
+++ b/reals/fast/CRexp.v
@@ -28,7 +28,7 @@ Require Import CoRN.reals.fast.CRstreams.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRIR.
 Require Import CoRN.reals.iso_CReals.
-Require Import Coq.QArith.Qpower.
+From Coq Require Import Qpower.
 Require Import CoRN.algebra.COrdFields2.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.transc.PowerSeries.
@@ -40,8 +40,8 @@ Require Import CoRN.reals.fast.ModulusDerivative.
 Require Import CoRN.reals.fast.ContinuousCorrect.
 Require Import CoRN.reals.fast.CRsign.
 Require Import CoRN.reals.Q_in_CReals.
-Require Import Coq.QArith.Qabs.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qabs.
+From Coq Require Import Qround.
 Require Import CoRN.tactics.CornTac.
 Require Import MathClasses.theory.int_pow.
 Require Import MathClasses.interfaces.abstract_algebra.
diff --git a/reals/fast/CRln.v b/reals/fast/CRln.v
index aa3b98e62..0c731079c 100644
--- a/reals/fast/CRln.v
+++ b/reals/fast/CRln.v
@@ -25,7 +25,7 @@ Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.reals.fast.CRartanh_slow.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRIR.
-Require Import Coq.QArith.Qpower.
+From Coq Require Import Qpower.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.reals.fast.ModulusDerivative.
 Require Import CoRN.reals.fast.ContinuousCorrect.
diff --git a/reals/fast/CRpower.v b/reals/fast/CRpower.v
index 4dd291c0b..2628a700e 100644
--- a/reals/fast/CRpower.v
+++ b/reals/fast/CRpower.v
@@ -23,8 +23,8 @@ Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.ProductMetric.
 Require Import CoRN.reals.fast.CRArith.
-Require Import Coq.QArith.Qpower.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qpower.
+From Coq Require Import Qabs.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.model.totalorder.QposMinMax. 
diff --git a/reals/fast/CRroot.v b/reals/fast/CRroot.v
index 910087035..44873b0ba 100644
--- a/reals/fast/CRroot.v
+++ b/reals/fast/CRroot.v
@@ -30,7 +30,7 @@ Require Import CoRN.reals.NRootIR.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.model.totalorder.QposMinMax.
 Require Import CoRN.model.metric2.Qmetric.
-Require Import Coq.QArith.Qpower.
+From Coq Require Import Qpower.
 Require Import CoRN.model.ordfields.Qordfield.
 Require Import CoRN.reals.fast.Compress.
 Require Import CoRN.reals.fast.PowerBound.
diff --git a/reals/fast/CRsin.v b/reals/fast/CRsin.v
index b4aa2876f..03536d510 100644
--- a/reals/fast/CRsin.v
+++ b/reals/fast/CRsin.v
@@ -30,9 +30,9 @@ Require Import CoRN.reals.fast.CRexp.
 Require Import CoRN.reals.fast.CRpi.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRIR.
-Require Import Coq.QArith.Qpower Coq.QArith.Qabs.
+From Coq Require Import Qpower Qabs.
 Require Import CoRN.model.ordfields.Qordfield.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qround.
 Require Import CoRN.transc.Pi.
 Require Import CoRN.reals.fast.ModulusDerivative.
 Require Import CoRN.reals.fast.ContinuousCorrect.
diff --git a/reals/fast/CRstreams.v b/reals/fast/CRstreams.v
index 19d037bf8..95e484ea8 100644
--- a/reals/fast/CRstreams.v
+++ b/reals/fast/CRstreams.v
@@ -24,11 +24,12 @@ Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.model.totalorder.QposMinMax.
 Require Import CoRN.model.metric2.Qmetric. 
 Require Import CoRN.metric2.Limit.
-Require Import Coq.QArith.Qabs. 
-Require Import Coq.Arith.Arith.
-Require Import Coq.QArith.Qpower.
-Require Import CoRN.reals.fast.LazyNat. 
-Require Import Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.streams.
+From Coq Require Import Qabs.
+From Coq Require Import Arith.
+From Coq Require Import Qpower.
+Require Import CoRN.reals.fast.LazyNat.
+From Coq Require Import Ring.
+Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.streams.
 Require Export MathClasses.theory.series.
 Require Import MathClasses.interfaces.abstract_algebra MathClasses.theory.streams.
 
diff --git a/reals/fast/Compress.v b/reals/fast/Compress.v
index 1e4fe00b2..d27b61e81 100644
--- a/reals/fast/Compress.v
+++ b/reals/fast/Compress.v
@@ -25,7 +25,7 @@ Require Import CoRN.metric2.UniformContinuity.
 Require Import CoRN.model.totalorder.QposMinMax.
 Require Export CoRN.model.metric2.CRmetric.
 Require Import CoRN.model.metric2.Qmetric.
-Require Import Coq.ZArith.Zdiv.
+From Coq Require Import Zdiv.
 
 Opaque CR.
 
diff --git a/reals/fast/Integration.v b/reals/fast/Integration.v
index 5b12d1ccd..22a3cc7ee 100644
--- a/reals/fast/Integration.v
+++ b/reals/fast/Integration.v
@@ -32,9 +32,9 @@ Require Import CoRN.model.structures.StepQsec.
 Require Import CoRN.model.structures.OpenUnit.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.tactics.Qauto.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qround.
 Require Import CoRN.model.metric2.L1metric.
 Require Import CoRN.model.metric2.LinfMetric.
 Require Import CoRN.model.ordfields.Qordfield.
diff --git a/reals/fast/Interval.v b/reals/fast/Interval.v
index 915e3fa06..fdc20238b 100644
--- a/reals/fast/Interval.v
+++ b/reals/fast/Interval.v
@@ -27,8 +27,8 @@ Require Export CoRN.metric2.LocatedSubset.
 Require Export CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRabs.
 Require Export CoRN.model.metric2.Qmetric.
-Require Import Coq.QArith.Qround.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qround.
+From Coq Require Import Qabs.
 Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.logic.Classic.
 
diff --git a/reals/fast/MultivariatePolynomials.v b/reals/fast/MultivariatePolynomials.v
index 8ae34d248..4e8872582 100644
--- a/reals/fast/MultivariatePolynomials.v
+++ b/reals/fast/MultivariatePolynomials.v
@@ -9,7 +9,7 @@ Require Import CoRN.model.totalorder.QMinMax.
 Require Import CoRN.tactics.CornTac.
 Require Import CoRN.tactics.Qauto.
 Require Import CoRN.model.metric2.Qmetric.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qabs.
 Require Import CoRN.reals.fast.CRabs.
 Require Import CoRN.reals.fast.ModulusDerivative.
 Require Import CoRN.reals.fast.CRArith.
diff --git a/reals/fast/Plot.v b/reals/fast/Plot.v
index 02436ee63..d1254fb2f 100644
--- a/reals/fast/Plot.v
+++ b/reals/fast/Plot.v
@@ -18,7 +18,7 @@ COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
 IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 *)
-Require Import QArith.Qround.
+From Coq Require Import Qround.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.ProductMetric.
 Require Import CoRN.metric2.UniformContinuity.
diff --git a/reals/fast/PowerBound.v b/reals/fast/PowerBound.v
index 4789d7437..067ec5c71 100644
--- a/reals/fast/PowerBound.v
+++ b/reals/fast/PowerBound.v
@@ -22,9 +22,9 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Program.Basics.
-Require Import Coq.QArith.Qpower.
+From Coq Require Import ZArith.
+From Coq Require Import Basics.
+From Coq Require Import Qpower.
 Require Import CoRN.stdlib_omissions.Z.
 
 Lemma Psize_Zlog2 (p: positive) :
diff --git a/reals/fast/RasterizeQ.v b/reals/fast/RasterizeQ.v
index 57294b303..c8e7b8e3e 100644
--- a/reals/fast/RasterizeQ.v
+++ b/reals/fast/RasterizeQ.v
@@ -25,8 +25,8 @@ Require Export CoRN.reals.fast.RasterQ.
 Require Import CoRN.reals.fast.Interval.
 Require Import CoRN.logic.Classic.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.QArith.Qabs.
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qabs.
+From Coq Require Import Qround.
 
 Local Open Scope Q_scope.
 
diff --git a/reals/fast/uneven_CRplus.v b/reals/fast/uneven_CRplus.v
index 1935347ae..3236ab290 100644
--- a/reals/fast/uneven_CRplus.v
+++ b/reals/fast/uneven_CRplus.v
@@ -1,8 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-        Coq.QArith.QArith CoRN.model.totalorder.QposMinMax
+From Coq Require Import QArith.
+Require Import CoRN.model.totalorder.QposMinMax
         CoRN.model.metric2.Qmetric CoRN.reals.fast.CRArith.
 
 (** The approximation function for CRplus results distributes a given error evenly
diff --git a/reals/faster/ACarith.v b/reals/faster/ACarith.v
index d0a759865..c156e1838 100644
--- a/reals/faster/ACarith.v
+++ b/reals/faster/ACarith.v
@@ -1,9 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.QArith.Qabs
-  CoRN.model.metric2.Qmetric
+From Coq Require Import Qabs.
+Require Import CoRN.model.metric2.Qmetric
   CoRN.metric2.ProductMetric
   CoRN.model.totalorder.QposMinMax 
   CoRN.model.totalorder.QMinMax
diff --git a/reals/faster/AQmetric.v b/reals/faster/AQmetric.v
index f9a5a2299..005b7caa4 100644
--- a/reals/faster/AQmetric.v
+++ b/reals/faster/AQmetric.v
@@ -1,7 +1,7 @@
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import 
-  Coq.Program.Program Coq.setoid_ring.Ring CoRN.util.Qdlog
+From Coq Require Import Program Ring.
+Require Import CoRN.util.Qdlog
   CoRN.model.totalorder.QposMinMax
   CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.metric2.MetricMorphisms.
 Require Export
diff --git a/reals/faster/ARAlternatingSum.v b/reals/faster/ARAlternatingSum.v
index df3c340af..966329e87 100644
--- a/reals/faster/ARAlternatingSum.v
+++ b/reals/faster/ARAlternatingSum.v
@@ -1,6 +1,5 @@
-Require Import 
-        Coq.QArith.Qabs
-        CoRN.util.Qdlog
+From Coq Require Import Qabs.
+Require Import CoRN.util.Qdlog
         CoRN.algebra.RSetoid
         CoRN.model.totalorder.QposMinMax
         CoRN.model.metric2.Qmetric
diff --git a/reals/faster/ARArith.v b/reals/faster/ARArith.v
index d7f21706d..8eec76760 100644
--- a/reals/faster/ARArith.v
+++ b/reals/faster/ARArith.v
@@ -1,9 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import 
-  Coq.Program.Program Coq.setoid_ring.Ring
-  Coq.QArith.Qabs CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics
+From Coq Require Import Program Ring Qabs.
+Require Import CoRN.stdlib_omissions.Q MathClasses.misc.workaround_tactics
   CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.util.Qdlog
   CoRN.metric2.Complete CoRN.metric2.Prelength CoRN.model.metric2.Qmetric CoRN.metric2.MetricMorphisms 
   CoRN.reals.fast.CRArith CoRN.reals.fast.CRpower
diff --git a/reals/faster/ARQ.v b/reals/faster/ARQ.v
index 7fdb3cce6..6f0f13300 100644
--- a/reals/faster/ARQ.v
+++ b/reals/faster/ARQ.v
@@ -1,8 +1,10 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.QArith.QArith CoRN.util.Qdlog Coq.ZArith.ZArith CoRN.reals.fast.Compress
+From Coq Require Import QArith.
+Require Import CoRN.util.Qdlog.
+From Coq Require Import ZArith.
+Require Import CoRN.reals.fast.Compress
   CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.reals.faster.ARArith
   CoRN.model.totalorder.QposMinMax.
 
diff --git a/reals/faster/ARabs.v b/reals/faster/ARabs.v
index 4014829d6..be4eccded 100644
--- a/reals/faster/ARabs.v
+++ b/reals/faster/ARabs.v
@@ -1,9 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.QArith.Qabs
-  CoRN.model.metric2.Qmetric
+From Coq Require Import Qabs.
+Require Import CoRN.model.metric2.Qmetric
   CoRN.model.totalorder.QposMinMax 
   CoRN.model.totalorder.QMinMax
   CoRN.reals.fast.CRabs 
diff --git a/reals/faster/ARbigD.v b/reals/faster/ARbigD.v
index 976ee2454..51224e521 100644
--- a/reals/faster/ARbigD.v
+++ b/reals/faster/ARbigD.v
@@ -1,8 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ 
+From Coq Require Import Program QArith ZArith.
+Require Import Bignums.BigZ.BigZ 
   CoRN.model.totalorder.QposMinMax 
   CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.util.Qdlog CoRN.reals.faster.ARArith
   MathClasses.theory.int_pow MathClasses.theory.nat_pow
diff --git a/reals/faster/ARbigQ.v b/reals/faster/ARbigQ.v
index e9dff6a45..1877925f0 100644
--- a/reals/faster/ARbigQ.v
+++ b/reals/faster/ARbigQ.v
@@ -1,8 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.Program.Program Coq.QArith.QArith Coq.ZArith.ZArith Bignums.BigZ.BigZ Bignums.BigQ.BigQ 
+From Coq Require Import Program QArith ZArith.
+Require Import Bignums.BigZ.BigZ Bignums.BigQ.BigQ 
   CoRN.reals.fast.Compress CoRN.reals.faster.ARQ
   CoRN.metric2.MetricMorphisms CoRN.model.metric2.Qmetric CoRN.reals.faster.ARArith
   MathClasses.implementations.stdlib_rationals MathClasses.implementations.stdlib_binary_integers MathClasses.implementations.field_of_fractions
diff --git a/reals/faster/ARexp.v b/reals/faster/ARexp.v
index 63106bcd3..82d61b7c2 100644
--- a/reals/faster/ARexp.v
+++ b/reals/faster/ARexp.v
@@ -1,11 +1,12 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.Program.Program MathClasses.misc.workaround_tactics
+From Coq Require Import Program.
+Require Import MathClasses.misc.workaround_tactics
   CoRN.model.totalorder.QposMinMax 
-  CoRN.model.totalorder.QMinMax Coq.QArith.Qround Coq.QArith.Qabs
-  CoRN.util.Qdlog CoRN.stdlib_omissions.Q 
+  CoRN.model.totalorder.QMinMax.
+From Coq Require Import Qround Qabs.
+Require Import CoRN.util.Qdlog CoRN.stdlib_omissions.Q 
   CoRN.reals.fast.CRexp CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum
   CoRN.reals.fast.Compress CoRN.reals.fast.CRpower
   CoRN.metric2.MetricMorphisms CoRN.reals.faster.ARAlternatingSum MathClasses.interfaces.abstract_algebra 
diff --git a/reals/faster/ARinterval.v b/reals/faster/ARinterval.v
index 986f045fe..86c52fccb 100644
--- a/reals/faster/ARinterval.v
+++ b/reals/faster/ARinterval.v
@@ -1,9 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.QArith.Qabs Coq.QArith.Qround
-  CoRN.model.metric2.Qmetric
+From Coq Require Import Qabs Qround.
+Require Import CoRN.model.metric2.Qmetric
   CoRN.metric2.ProductMetric
   CoRN.metric2.Prelength
   CoRN.metric2.Compact
diff --git a/reals/faster/ARplot.v b/reals/faster/ARplot.v
index fdb28ca09..73bcea7fc 100644
--- a/reals/faster/ARplot.v
+++ b/reals/faster/ARplot.v
@@ -1,4 +1,4 @@
-Require Import Coq.QArith.Qround.
+From Coq Require Import Qround.
 Require Import CoRN.reals.fast.Plot.
 Require Import CoRN.reals.faster.ARArith.
 Require Import CoRN.reals.faster.ARinterval.
diff --git a/reals/faster/ARroot.v b/reals/faster/ARroot.v
index df6a68f4e..3035ed3ff 100644
--- a/reals/faster/ARroot.v
+++ b/reals/faster/ARroot.v
@@ -1,10 +1,12 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import
-  Coq.setoid_ring.Ring CoRN.stdlib_omissions.Z
+From Coq Require Import Ring.
+Require Import CoRN.stdlib_omissions.Z
   CoRN.model.totalorder.QposMinMax 
-  CoRN.metric2.Complete CoRN.model.metric2.Qmetric Coq.ZArith.ZArith CoRN.util.Qdlog
+  CoRN.metric2.Complete CoRN.model.metric2.Qmetric.
+From Coq Require Import ZArith.
+Require Import CoRN.util.Qdlog
   CoRN.reals.fast.CRroot
   CoRN.reals.faster.ARabs
   MathClasses.interfaces.abstract_algebra MathClasses.theory.shiftl MathClasses.theory.nat_pow MathClasses.theory.int_pow.
diff --git a/reals/faster/ARsign.v b/reals/faster/ARsign.v
index 79cc37e4c..4662493f1 100644
--- a/reals/faster/ARsign.v
+++ b/reals/faster/ARsign.v
@@ -1,7 +1,8 @@
 Require Import CoRN.algebra.RSetoid.
 Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
-Require Import Coq.ZArith.ZArith CoRN.reals.faster.ARArith.
+From Coq Require Import ZArith.
+Require Import CoRN.reals.faster.ARArith.
 
 Ltac AR_solve_pos_loop k :=
  (apply AR_epsilon_sign_dec_pos with k;
diff --git a/reals/faster/ARsin.v b/reals/faster/ARsin.v
index 29692af6b..f590572b2 100644
--- a/reals/faster/ARsin.v
+++ b/reals/faster/ARsin.v
@@ -1,6 +1,5 @@
-Require Import
-  Coq.QArith.Qround Coq.QArith.Qpower 
-  MathClasses.interfaces.abstract_algebra 
+From Coq Require Import Qround Qpower.
+Require Import MathClasses.interfaces.abstract_algebra 
   MathClasses.theory.nat_pow
   MathClasses.theory.int_pow
   CoRN.algebra.RSetoid
diff --git a/reals/faster/ApproximateRationals.v b/reals/faster/ApproximateRationals.v
index c3a1b3cb7..07666a56b 100644
--- a/reals/faster/ApproximateRationals.v
+++ b/reals/faster/ApproximateRationals.v
@@ -3,11 +3,12 @@ Require Import CoRN.metric2.Metric.
 Require Import CoRN.metric2.UniformContinuity.
 Require
   MathClasses.implementations.stdlib_rationals MathClasses.implementations.positive_semiring_elements.
-Require Import 
-  Coq.Program.Program
-  CoRN.model.totalorder.QposMinMax
+From Coq Require Import Program.
+Require Import CoRN.model.totalorder.QposMinMax
   MathClasses.misc.workaround_tactics
-  CoRN.stdlib_omissions.Q CoRN.util.Qdlog CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.classes.Qclasses CoRN.model.totalorder.QMinMax
+  CoRN.stdlib_omissions.Q CoRN.util.Qdlog CoRN.model.metric2.Qmetric.
+From Coq Require Import Qabs.
+Require Import CoRN.classes.Qclasses CoRN.model.totalorder.QMinMax
   CoRN.algebra.RSetoid CoRN.metric2.MetricMorphisms
   MathClasses.orders.minmax MathClasses.orders.dec_fields MathClasses.theory.abs MathClasses.theory.shiftl MathClasses.theory.int_pow.
 Require Export
diff --git a/reals/stdlib/CMTIntegrableSets.v b/reals/stdlib/CMTIntegrableSets.v
index e01e9bf67..6f4a5e4de 100644
--- a/reals/stdlib/CMTIntegrableSets.v
+++ b/reals/stdlib/CMTIntegrableSets.v
@@ -26,14 +26,14 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI
    unnecessary concept of complemented set.
  *)
 
-Require Import Logic.ConstructiveEpsilon.
-Require Import QArith.
-Require Import ConstructiveReals.
-Require Import ConstructiveAbs.
-Require Import ConstructiveMinMax.
-Require Import ConstructiveSum.
-Require Import ConstructivePower.
-Require Import ConstructiveLimits.
+From Coq Require Import ConstructiveEpsilon.
+From Coq Require Import QArith.
+From Coq Require Import ConstructiveReals.
+From Coq Require Import ConstructiveAbs.
+From Coq Require Import ConstructiveMinMax.
+From Coq Require Import ConstructiveSum.
+From Coq Require Import ConstructivePower.
+From Coq Require Import ConstructiveLimits.
 Require Import ConstructiveDiagonal.
 Require Import ConstructivePartialFunctions.
 
diff --git a/reals/stdlib/ConstructiveFastReals.v b/reals/stdlib/ConstructiveFastReals.v
index ff07ad41e..0beff6c9c 100644
--- a/reals/stdlib/ConstructiveFastReals.v
+++ b/reals/stdlib/ConstructiveFastReals.v
@@ -12,14 +12,14 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI
 (** Proof that CoRN's fast reals implement the standard library's
     interface ConstructiveReals. *)
 
-Require Import Coq.Reals.Abstract.ConstructiveReals.
+From Coq Require Import ConstructiveReals.
 Require Import CoRN.model.metric2.Qmetric.
 Require Import CoRN.model.metric2.CRmetric.
 Require Import CoRN.reals.fast.CRFieldOps.
 Require Import CoRN.reals.fast.CRArith.
 Require Import CoRN.reals.fast.CRabs.
 Require Import CoRN.model.totalorder.QposMinMax.
-Require Import Coq.Logic.ConstructiveEpsilon.
+From Coq Require Import ConstructiveEpsilon.
 
 Lemma CRltT_linear : @isLinearOrder (RegularFunction Qball) CRltT.
 Proof.
diff --git a/reals/stdlib/Markov.v b/reals/stdlib/Markov.v
index bcffcf1cd..aa20ed29f 100644
--- a/reals/stdlib/Markov.v
+++ b/reals/stdlib/Markov.v
@@ -10,9 +10,9 @@ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLI
 
 (** Consequence of the Markov principle on constructive reals. *)
 
-Require Import Coq.QArith.QArith_base.
-Require Import Coq.Reals.Abstract.ConstructiveReals.
-Require Import Coq.Reals.Abstract.ConstructiveAbs.
+From Coq Require Import QArith_base.
+From Coq Require Import ConstructiveReals.
+From Coq Require Import ConstructiveAbs.
 
 Local Open Scope ConstructiveReals.
 
diff --git a/stdlib_omissions/Q.v b/stdlib_omissions/Q.v
index 2e645247f..4c731c04e 100644
--- a/stdlib_omissions/Q.v
+++ b/stdlib_omissions/Q.v
@@ -1,7 +1,5 @@
-Require Import
-  Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith
-  Coq.QArith.Qpower Coq.QArith.Qround
-  Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List.
+From Coq Require Import QArith ZArith NArith Qpower Qround Qround Qabs.
+Require Import CoRN.stdlib_omissions.List.
 
 Require CoRN.stdlib_omissions.Z.
 
diff --git a/stdlib_omissions/Z.v b/stdlib_omissions/Z.v
index 598314b8a..ba4d4af07 100644
--- a/stdlib_omissions/Z.v
+++ b/stdlib_omissions/Z.v
@@ -1,6 +1,7 @@
 
-Require Import Coq.ZArith.ZArith CoRN.stdlib_omissions.P.
-Require Import Lia.
+From Coq Require Import ZArith.
+Require Import CoRN.stdlib_omissions.P.
+From Coq Require Import Lia.
 
 (*Require Import NSigNAxioms.  was added in the trunk branch*)
 
diff --git a/tactics/Qauto.v b/tactics/Qauto.v
index deb73256c..7da7cc937 100644
--- a/tactics/Qauto.v
+++ b/tactics/Qauto.v
@@ -21,8 +21,8 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF.
 
 Require Export CoRN.model.ordfields.Qordfield.
 Require Import CoRN.algebra.COrdFields2.
-Require Import Coq.QArith.Qpower.
-Require Import Coq.QArith.Qabs.
+From Coq Require Import Qpower.
+From Coq Require Import Qabs.
 
 (*Require Import CoRN.tactics.CornTac. 
 was removed in the trunk branch
diff --git a/util/Extract.v b/util/Extract.v
index 997f05b59..c4e20e554 100644
--- a/util/Extract.v
+++ b/util/Extract.v
@@ -1,3 +1,4 @@
+From Coq Require Import Extraction.
 Require Import CoRN.reals.fast.CRtrans.
 
 Extraction Language Haskell.
diff --git a/util/PointFree.v b/util/PointFree.v
index 62442d0da..2ab273041 100644
--- a/util/PointFree.v
+++ b/util/PointFree.v
@@ -1,4 +1,5 @@
-Require Import Coq.Program.Program Coq.Unicode.Utf8 CoRN.stdlib_omissions.Pair.
+From Coq Require Import Program Utf8.
+Require Import CoRN.stdlib_omissions.Pair.
 Generalizable All Variables.
 
 (** In the following type class, r is an "output parameter" in the sense
diff --git a/util/Qdlog.v b/util/Qdlog.v
index 3e0254bbe..07c1fd658 100644
--- a/util/Qdlog.v
+++ b/util/Qdlog.v
@@ -1,6 +1,6 @@
 (* Discrete logarithm with base 2 and 4 on [Q] *)
-Require Import 
-  Coq.ZArith.ZArith Coq.QArith.QArith Coq.QArith.Qround CoRN.stdlib_omissions.Q
+From Coq Require Import ZArith QArith Qround.
+Require Import CoRN.stdlib_omissions.Q
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
   MathClasses.theory.int_pow MathClasses.orders.rationals MathClasses.implementations.stdlib_rationals MathClasses.implementations.positive_semiring_elements.
 
diff --git a/util/Qgcd.v b/util/Qgcd.v
index 2d0c4967b..7a3aef3ae 100644
--- a/util/Qgcd.v
+++ b/util/Qgcd.v
@@ -1,6 +1,5 @@
-
-Require Import
-        Coq.QArith.QArith CoRN.model.Zmod.ZGcd
+From Coq Require Import QArith.
+Require Import CoRN.model.Zmod.ZGcd
         CoRN.model.totalorder.QposMinMax
         CoRN.stdlib_omissions.Q.
 
diff --git a/util/Qsums.v b/util/Qsums.v
index 72a84fd36..ac2e4383e 100644
--- a/util/Qsums.v
+++ b/util/Qsums.v
@@ -1,10 +1,9 @@
-Require Import
-  CoRN.stdlib_omissions.List
-  Coq.QArith.QArith Coq.QArith.Qabs
-  CoRN.model.totalorder.QposMinMax 
-  CoRN.model.metric2.Qmetric
-  Coq.Program.Program
-  CoRN.stdlib_omissions.N
+Require Import CoRN.stdlib_omissions.List.
+From Coq Require Import QArith Qabs.
+Require Import CoRN.model.totalorder.QposMinMax
+  CoRN.model.metric2.Qmetric.
+From Coq Require Import Program.
+Require Import CoRN.stdlib_omissions.N
   CoRN.stdlib_omissions.Z
   CoRN.stdlib_omissions.Q.