diff --git a/Makefile.common b/Makefile.common
index fb7aa162da..2691bd4fad 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -117,7 +117,7 @@ doc: __always__ Makefile.coq
 #	cd _build_doc && grep -v vio: .Makefile.coq.d > depend
 #	cd _build_doc && cat depend | $(MATHCOMP)etc/buildlibgraph $(COQFILES) > htmldoc/depend.js
 	cd _build_doc && $(COQBIN)coqdoc -t "MathComp Analysis" \
-		-g --utf8 -R classical mathcomp.classical -R theories mathcomp.analysis \
+		-g --utf8 -Q classical mathcomp.classical -Q theories mathcomp.analysis \
 		--parse-comments \
 		--multi-index $(COQFILES) -d htmldoc
 	. $(MATHCOMP)etc/utils/builddoc_lib.sh; \
diff --git a/_CoqProject b/_CoqProject
index 4261f8dcb4..e4068f17e3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,5 @@
--R classical mathcomp.classical
--R theories mathcomp.analysis
+-Q classical mathcomp.classical
+-Q theories mathcomp.analysis
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
diff --git a/classical/Make b/classical/Make
index 45c406b116..80e2337294 100644
--- a/classical/Make
+++ b/classical/Make
@@ -1,4 +1,4 @@
--R . mathcomp.classical
+-Q . mathcomp.classical
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 9b4f5ad370..dae167d93a 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
-Require Import BinPos.
+From Coq Require Import BinPos.
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From mathcomp Require Import finset interval.
 
diff --git a/classical/wochoice.v b/classical/wochoice.v
index 43f5593ad0..9a4652a0bc 100644
--- a/classical/wochoice.v
+++ b/classical/wochoice.v
@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-Require Import boolp contra.
+From mathcomp Require Import boolp contra.
 
 (**md**************************************************************************)
 (* # Well-ordered choice                                                      *)
diff --git a/theories/Make b/theories/Make
index 26289e19d7..17e5da2d45 100644
--- a/theories/Make
+++ b/theories/Make
@@ -1,4 +1,4 @@
--R . mathcomp.analysis
+-Q . mathcomp.analysis
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
index 2946c2da9f..ed64108796 100644
--- a/theories/Rstruct.v
+++ b/theories/Rstruct.v
@@ -25,9 +25,9 @@ liability. See the COPYING file for more details.
 (* # Compatibility with the real numbers of Coq                               *)
 (******************************************************************************)
 
-Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
-Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
-Require Import Rtrigo1 Reals.
+From Coq Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
+From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
+From Coq Require Import Rtrigo1 Reals.
 From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
 From mathcomp Require Import archimedean.
 From HB Require Import structures.
@@ -364,7 +364,7 @@ End ssreal_struct.
 
 Local Open Scope ring_scope.
 From mathcomp Require Import boolp classical_sets.
-Require Import reals.
+From mathcomp Require Import reals.
 
 Section ssreal_struct_contd.
 Implicit Type E : set R.
@@ -424,7 +424,7 @@ Implicit Types (x y : R) (m n : nat).
 
 (* equational lemmas about exp, sin and cos for mathcomp compat *)
 
-(* Require Import realsum. *)
+(* From mathcomp Require Import realsum. *)
 
 (* :TODO: One day, do this *)
 (* Notation "\Sum_ i E" := (psum (fun i => E)) *)
@@ -697,7 +697,7 @@ End bigmaxr.
 
 End ssreal_struct_contd.
 
-Require Import signed topology.
+From mathcomp Require Import signed topology.
 
 Section analysis_struct.
 
diff --git a/theories/altreals/dedekind.v b/theories/altreals/dedekind.v
index ccb2bb31df..cfc4cb8251 100644
--- a/theories/altreals/dedekind.v
+++ b/theories/altreals/dedekind.v
@@ -8,7 +8,7 @@
 
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra.
-(* ------- *) Require Import Setoid.
+From Coq Require Import Setoid.
 
 (* -------------------------------------------------------------------- *)
 Set   Implicit Arguments.
diff --git a/theories/altreals/discrete.v b/theories/altreals/discrete.v
index d2b0f71e9f..029af438e5 100644
--- a/theories/altreals/discrete.v
+++ b/theories/altreals/discrete.v
@@ -7,8 +7,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.
-Require Import xfinmap reals.
-(* ------- *) Require (*--*) Setoid.
+From mathcomp Require Import xfinmap reals.
+From Coq Require Setoid.
 
 (* -------------------------------------------------------------------- *)
 Set   Implicit Arguments.
diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v
index 1402f3e310..0ad57d5412 100644
--- a/theories/altreals/distr.v
+++ b/theories/altreals/distr.v
@@ -6,8 +6,8 @@
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp classical_sets mathcomp_extra.
-Require Import xfinmap constructive_ereal reals discrete.
-Require Import realseq realsum.
+From mathcomp Require Import xfinmap constructive_ereal reals discrete.
+From mathcomp Require Import realseq realsum.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v
index ddeb3f3a79..f8d1d909e1 100644
--- a/theories/altreals/realseq.v
+++ b/theories/altreals/realseq.v
@@ -5,10 +5,10 @@
 
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra.
-Require Import mathcomp.bigenough.bigenough.
+From mathcomp Require Import bigenough.
 From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import mathcomp_extra.
-Require Import xfinmap constructive_ereal reals discrete.
+From mathcomp Require Import xfinmap constructive_ereal reals discrete.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index 2cb29ac962..6c09eb180f 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -5,7 +5,7 @@
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp.classical Require Import boolp.
-Require Import xfinmap constructive_ereal reals discrete realseq.
+From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions.
 
 Set Implicit Arguments.
diff --git a/theories/cantor.v b/theories/cantor.v
index 06b7463b25..8006e1ced2 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -3,8 +3,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat.
 From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality.
-Require Import reals signed topology function_spaces separation_axioms.
+From mathcomp Require Import cardinality reals signed.
+From mathcomp Require Import topology function_spaces separation_axioms.
 
 (**md**************************************************************************)
 (* # The Cantor Space and Applications                                        *)
diff --git a/theories/charge.v b/theories/charge.v
index 0e35a7dd72..7e2d07f48b 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -4,8 +4,9 @@ From mathcomp Require Import finmap fingroup perm rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality.
 From mathcomp Require Import functions fsbigop set_interval.
 From HB Require Import structures.
-Require Import reals ereal signed topology numfun normedtype sequences.
-Require Import esum measure realfun lebesgue_measure lebesgue_integral.
+From mathcomp Require Import reals ereal signed topology numfun normedtype.
+From mathcomp Require Import sequences esum measure realfun lebesgue_measure.
+From mathcomp Require Import lebesgue_integral.
 
 (**md**************************************************************************)
 (* # Charges                                                                  *)
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index f1a0d1cee6..a2155ef0e1 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -11,8 +11,7 @@
    bounds of intervals*)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap.
-From mathcomp Require Import mathcomp_extra.
-Require Import signed.
+From mathcomp Require Import mathcomp_extra signed.
 
 (**md**************************************************************************)
 (* # Extended real numbers $\overline{R}$                                     *)
diff --git a/theories/convex.v b/theories/convex.v
index d9bf76a322..dde76d9a14 100644
--- a/theories/convex.v
+++ b/theories/convex.v
@@ -2,9 +2,9 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
 From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
-From mathcomp Require Import functions cardinality.
-Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
-Require Import realfun itv.
+From mathcomp Require Import functions cardinality ereal reals signed.
+From mathcomp Require Import topology prodnormedzmodule normedtype derive.
+From mathcomp Require Import realfun itv.
 From HB Require Import structures.
 
 (**md**************************************************************************)
diff --git a/theories/derive.v b/theories/derive.v
index 67d42a07fd..2102ced25e 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2,7 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-Require Import reals signed topology prodnormedzmodule normedtype landau forms.
+From mathcomp Require Import reals signed topology prodnormedzmodule normedtype.
+From mathcomp Require Import landau forms.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)
diff --git a/theories/ereal.v b/theories/ereal.v
index b6109da43f..015c0e0207 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -8,8 +8,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import fsbigop cardinality set_interval.
-Require Import reals signed topology.
-Require Export constructive_ereal.
+From mathcomp Require Import reals signed topology.
+From mathcomp Require Export constructive_ereal.
 
 (**md**************************************************************************)
 (* # Extended real numbers, classical part ($\overline{\mathbb{R}}$)          *)
diff --git a/theories/esum.v b/theories/esum.v
index 241e6fbe59..57959228b9 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop.
-Require Import reals ereal signed topology sequences normedtype numfun.
+From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import topology sequences normedtype numfun.
 
 (**md**************************************************************************)
 (* # Summation over classical sets                                            *)
diff --git a/theories/exp.v b/theories/exp.v
index 382914f93f..bf6f2f0ff0 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -2,10 +2,9 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions.
-From mathcomp Require Import mathcomp_extra.
-Require Import reals ereal.
-Require Import signed topology normedtype landau sequences derive realfun.
-Require Import itv convex.
+From mathcomp Require Import mathcomp_extra reals ereal signed.
+From mathcomp Require Import topology normedtype landau sequences derive.
+From mathcomp Require Import realfun itv convex.
 
 (**md**************************************************************************)
 (* # Theory of exponential/logarithm functions                                *)
diff --git a/theories/ftc.v b/theories/ftc.v
index 4e41c0198f..0a65b63ec1 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -2,10 +2,10 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop .
-Require Import signed reals ereal topology normedtype sequences real_interval.
-Require Import esum measure lebesgue_measure numfun realfun lebesgue_integral.
-Require Import derive charge.
+From mathcomp Require Import cardinality fsbigop signed reals ereal.
+From mathcomp Require Import topology normedtype sequences real_interval.
+From mathcomp Require Import esum measure lebesgue_measure numfun realfun.
+From mathcomp Require Import lebesgue_integral derive charge.
 
 (**md**************************************************************************)
 (* # Fundamental Theorem of Calculus for the Lebesgue Integral                *)
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index fcc1a68e85..05cc4d0c85 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-Require Import reals signed topology separation_axioms.
+From mathcomp Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 38ff6ee925..80685842a7 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -2,10 +2,10 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop .
-Require Import signed reals ereal topology normedtype sequences real_interval.
-Require Import esum measure lebesgue_measure lebesgue_integral numfun exp.
-Require Import convex itv.
+From mathcomp Require Import cardinality fsbigop signed reals ereal.
+From mathcomp Require Import topology normedtype sequences real_interval.
+From mathcomp Require Import esum measure lebesgue_measure lebesgue_integral.
+From mathcomp Require Import numfun exp convex itv.
 
 (**md**************************************************************************)
 (* # Hoelder's Inequality                                                     *)
diff --git a/theories/itv.v b/theories/itv.v
index b90c1580e6..3a4b37465f 100644
--- a/theories/itv.v
+++ b/theories/itv.v
@@ -3,8 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
 From mathcomp Require Import interval.
-From mathcomp Require Import mathcomp_extra boolp.
-Require Import signed.
+From mathcomp Require Import mathcomp_extra boolp signed.
 
 (**md**************************************************************************)
 (* # Numbers within an interval                                               *)
diff --git a/theories/kernel.v b/theories/kernel.v
index 6dad647865..3963473599 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -2,9 +2,9 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop.
-Require Import reals ereal signed topology normedtype sequences esum measure.
-Require Import numfun lebesgue_measure lebesgue_integral.
+From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import topology normedtype sequences esum measure.
+From mathcomp Require Import numfun lebesgue_measure lebesgue_integral.
 
 (**md**************************************************************************)
 (* # Kernels                                                                  *)
diff --git a/theories/landau.v b/theories/landau.v
index f3cf00dfc7..bee296e962 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -2,7 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-Require Import ereal reals signed topology normedtype prodnormedzmodule.
+From mathcomp Require Import ereal reals signed topology normedtype.
+From mathcomp Require Import prodnormedzmodule.
 
 (**md**************************************************************************)
 (* # Bachmann-Landau notations: $f=o(e)$, $f=O(e)$                            *)
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index bb0fda01b6..1c7b7ced67 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -3,9 +3,9 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop.
-Require Import signed reals ereal topology normedtype sequences real_interval.
-Require Import esum measure lebesgue_measure numfun realfun function_spaces.
+From mathcomp Require Import cardinality fsbigop signed reals ereal topology.
+From mathcomp Require Import normedtype sequences real_interval esum measure.
+From mathcomp Require Import lebesgue_measure numfun realfun function_spaces.
 
 (**md**************************************************************************)
 (* # Lebesgue Integral                                                        *)
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 8689a25297..f5bfa37808 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -2,11 +2,11 @@
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop.
-Require Import reals ereal signed topology numfun normedtype function_spaces.
+From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import topology numfun normedtype function_spaces.
 From HB Require Import structures.
-Require Import sequences esum measure real_interval realfun exp.
-Require Export lebesgue_stieltjes_measure.
+From mathcomp Require Import sequences esum measure real_interval realfun exp.
+From mathcomp Require Export lebesgue_stieltjes_measure.
 
 (**md**************************************************************************)
 (* # Lebesgue Measure                                                         *)
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 958eab237f..9e05ac8e7a 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -4,8 +4,8 @@ From mathcomp Require Import finmap fingroup perm rat archimedean.
 From HB Require Import structures.
 From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
 From mathcomp.classical Require Import functions fsbigop cardinality.
-Require Import reals ereal signed topology numfun normedtype sequences esum.
-Require Import real_interval measure realfun.
+From mathcomp Require Import reals ereal signed topology numfun normedtype.
+From mathcomp Require Import sequences esum real_interval measure realfun.
 
 (**md**************************************************************************)
 (* # Lebesgue Stieltjes Measure                                               *)
diff --git a/theories/measure.v b/theories/measure.v
index a00237c84e..f256cdce1c 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -1,8 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop.
-Require Import reals ereal signed topology normedtype sequences esum numfun.
+From mathcomp Require Import cardinality fsbigop reals ereal signed.
+From mathcomp Require Import topology normedtype sequences esum numfun.
 From HB Require Import structures.
 
 (**md**************************************************************************)
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 2363162ebd..bf6d1713aa 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -4,9 +4,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
-From mathcomp Require Import cardinality set_interval.
-Require Import ereal reals signed topology prodnormedzmodule function_spaces.
-Require Export separation_axioms.
+From mathcomp Require Import cardinality set_interval ereal reals.
+From mathcomp Require Import signed topology prodnormedzmodule function_spaces.
+From mathcomp Require Export separation_axioms.
 
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
diff --git a/theories/nsatz_realtype.v b/theories/nsatz_realtype.v
index 218346e2bf..a25a4c0f9f 100644
--- a/theories/nsatz_realtype.v
+++ b/theories/nsatz_realtype.v
@@ -1,7 +1,6 @@
-Require Import Nsatz.
+From Coq Require Import Nsatz.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum.
-From mathcomp Require Import boolp.
-Require Import reals ereal.
+From mathcomp Require Import boolp reals ereal.
 
 (**md**************************************************************************)
 (* # nsatz for realType                                                       *)
diff --git a/theories/numfun.v b/theories/numfun.v
index ac03207f62..f3361cce02 100644
--- a/theories/numfun.v
+++ b/theories/numfun.v
@@ -2,8 +2,9 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop.
-From mathcomp Require Import functions cardinality set_interval.
-Require Import signed reals ereal topology normedtype sequences function_spaces.
+From mathcomp Require Import functions cardinality set_interval signed reals.
+From mathcomp Require Import ereal topology normedtype sequences.
+From mathcomp Require Import function_spaces.
 
 (**md**************************************************************************)
 (* # Numerical functions                                                      *)
diff --git a/theories/probability.v b/theories/probability.v
index 3a6c382614..29ccb04736 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -4,9 +4,10 @@ From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop.
 From HB Require Import structures.
-Require Import exp numfun lebesgue_measure lebesgue_integral.
-Require Import reals ereal signed topology normedtype sequences esum measure.
-Require Import exp numfun lebesgue_measure lebesgue_integral kernel.
+From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral.
+From mathcomp Require Import reals ereal signed topology normedtype sequences.
+From mathcomp Require Import esum measure exp numfun lebesgue_measure.
+From mathcomp Require Import lebesgue_integral kernel.
 
 (**md**************************************************************************)
 (* # Probability                                                              *)
diff --git a/theories/prodnormedzmodule.v b/theories/prodnormedzmodule.v
index fcdfff5daa..0771324807 100644
--- a/theories/prodnormedzmodule.v
+++ b/theories/prodnormedzmodule.v
@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2020 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect fingroup ssralg poly ssrnum.
-Require Import signed.
+From mathcomp Require Import signed.
 
 (**md**************************************************************************)
 (* This file equips the product of two normedZmodTypes with a canonical       *)
diff --git a/theories/real_interval.v b/theories/real_interval.v
index 0577bc6acb..0e80b3a3de 100644
--- a/theories/real_interval.v
+++ b/theories/real_interval.v
@@ -4,7 +4,7 @@ From mathcomp Require Import fingroup perm rat archimedean finmap.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Export set_interval.
 From HB Require Import structures.
-Require Import reals ereal signed topology normedtype sequences.
+From mathcomp Require Import reals ereal signed topology normedtype sequences.
 
 (**md**************************************************************************)
 (* # Sets and intervals on $\overline{\mathbb{R}}$                            *)
diff --git a/theories/realfun.v b/theories/realfun.v
index 05046d38ce..bb902bfa2d 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -3,9 +3,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum archimedean.
 From mathcomp Require Import matrix interval zmodp vector fieldext falgebra.
 From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-From mathcomp Require Import cardinality.
-Require Import ereal reals signed topology prodnormedzmodule normedtype derive.
-Require Import sequences real_interval.
+From mathcomp Require Import cardinality ereal reals signed.
+From mathcomp Require Import topology prodnormedzmodule normedtype derive.
+From mathcomp Require Import sequences real_interval.
 From HB Require Import structures.
 
 (**md**************************************************************************)
diff --git a/theories/reals.v b/theories/reals.v
index c2dd629c57..5e0503ca13 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -42,7 +42,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.
 
-Require Import Setoid.
+From Coq Require Import Setoid.
 
 Declare Scope real_scope.
 
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index 453f254ede..4bf721ca0f 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -4,9 +4,7 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
-From mathcomp Require Import filter.
-Require Import reals signed.
-Require Export topology.
+From mathcomp Require Import filter reals signed topology.
 
 (**md**************************************************************************)
 (* # Separation Axioms                                                        *)
diff --git a/theories/sequences.v b/theories/sequences.v
index b09e633ba8..cc47871edc 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat archimedean.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import set_interval.
-Require Import reals ereal signed topology normedtype landau.
+From mathcomp Require Import reals ereal signed topology normedtype landau.
 
 (**md**************************************************************************)
 (* # Definitions and lemmas about sequences                                   *)
diff --git a/theories/showcase/summability.v b/theories/showcase/summability.v
index b2679d0274..9892dd9c9e 100644
--- a/theories/showcase/summability.v
+++ b/theories/showcase/summability.v
@@ -1,10 +1,10 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-Require Reals.
+From Coq Require Reals.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import interval zmodp.
 From mathcomp Require Import boolp classical_sets.
-Require Import ereal reals Rstruct signed topology normedtype.
+From mathcomp Require Import ereal reals Rstruct signed topology normedtype.
 
 (**md**************************************************************************)
 (* This file proposes a replacement for the definition `summable` (file       *)
diff --git a/theories/showcase/uniform_bigO.v b/theories/showcase/uniform_bigO.v
index dfb9d6a29e..5cf1f1180d 100644
--- a/theories/showcase/uniform_bigO.v
+++ b/theories/showcase/uniform_bigO.v
@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
-Require Import Reals.
+From Coq Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.
 From mathcomp Require Import boolp reals Rstruct ereal.
diff --git a/theories/topology.v b/theories/topology.v
index 7600e7f760..5d68ab01d5 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -5,7 +5,7 @@ From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 From mathcomp Require Export filter.
-Require Import reals signed.
+From mathcomp Require Import reals signed.
 
 (**md**************************************************************************)
 (* # Basic topological notions                                                *)
diff --git a/theories/trigo.v b/theories/trigo.v
index 86884d3ca7..e9c7aa313e 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -3,8 +3,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
-Require Import reals ereal nsatz_realtype signed topology normedtype landau.
-Require Import sequences derive realfun exp.
+From mathcomp Require Import reals ereal nsatz_realtype signed topology.
+From mathcomp Require Import normedtype landau sequences derive realfun exp.
 
 (**md**************************************************************************)
 (* # Theory of trigonometric functions                                        *)