Adapt to https://github.com/coq/coq/pull/19530

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.

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.

algebra/CSums.v

@@ -41,7 +41,7 @@
 (** printing Sumx %\ensuremath{\sum'}% #∑'&*)
 
 Require Export CoRN.algebra.CAbGroups.
-Require Export Coq.Arith.Peano_dec.
+From Coq Require Export Peano_dec.
 From Coq Require Import Lia.
 
 (**

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.
 

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.
 
 (**

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.

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.
 

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.
 

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.
 
 

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 | 

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.
 

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.
 

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.

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.
 

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.
 

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.

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.

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.

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.

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.

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.
 
 (**

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 :=

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.

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.
 

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.

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

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: *)

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># *)