Use From systematically

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; \

_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

classical/Make

@@ -1,4 +1,4 @@
--R . mathcomp.classical
+-Q . mathcomp.classical
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope

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

theories/Make

@@ -1,4 +1,4 @@
--R . mathcomp.analysis
+-Q . mathcomp.analysis
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope

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.
 

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.

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.

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 ereal reals discrete.
-Require Import topology realseq realsum.
+From mathcomp Require Import xfinmap ereal reals discrete.
+From mathcomp Require Import topology realseq realsum.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

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 ereal reals discrete topology.
+From mathcomp Require Import xfinmap ereal reals discrete topology.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

theories/altreals/realsum.v

@@ -5,9 +5,9 @@
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp.classical Require Import boolp.
-Require Import xfinmap ereal reals discrete realseq.
+From mathcomp Require Import xfinmap ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions.
-Require Import topology.
+From mathcomp Require Import topology.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

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

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

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}$                                     *)

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

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

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}}$)          *)

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

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

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

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

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

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

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

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

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

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

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

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

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 Rstruct.
-Require Import ereal reals signed topology prodnormedzmodule function_spaces.
-Require Export separation_axioms.
+From mathcomp Require Import cardinality set_interval Rstruct ereal reals.
+From mathcomp Require Import signed topology prodnormedzmodule function_spaces.
+From mathcomp Require Export separation_axioms.
 
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
@@ -1102,7 +1102,7 @@ Arguments cvgr0_norm_le {_ _ _ F FF}.
 Notation cvg_distP := fcvgrPdist_lt (only parsing).
 
 (* NB: the following section used to be in Rstruct.v *)
-Require Rstruct.
+From mathcomp Require Rstruct.
 
 Section analysis_struct.
 

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

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