Add a coq-mathcomp-reals package

_CoqProject

@@ -1,5 +1,9 @@
 -Q classical mathcomp.classical
+-Q reals mathcomp.reals
+-Q reals_stdlib mathcomp.reals_stdlib
+-Q altreals mathcomp.altreals
 -Q theories mathcomp.analysis
+-Q analysis_stdlib mathcomp.analysis_stdlib
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
@@ -20,26 +24,33 @@ classical/fsbigop.v
 classical/set_interval.v
 classical/classical_orders.v
 classical/filter.v
+reals/constructive_ereal.v
+reals/reals.v
+reals/real_interval.v
+reals/signed.v
+reals/itv.v
+reals/prodnormedzmodule.v
+reals/nsatz_realtype.v
+reals/all_reals.v
+altreals/xfinmap.v
+altreals/discrete.v
+altreals/realseq.v
+altreals/realsum.v
+altreals/distr.v
+reals_stdlib/Rstruct.v
 theories/all_analysis.v
-theories/constructive_ereal.v
 theories/ereal.v
-theories/reals.v
 theories/landau.v
-theories/Rstruct.v
-theories/Rstruct_topology.v
 theories/topology.v
 theories/separation_axioms.v
 theories/function_spaces.v
 theories/cantor.v
-theories/prodnormedzmodule.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v
 theories/exp.v
 theories/trigo.v
-theories/nsatz_realtype.v
 theories/esum.v
-theories/real_interval.v
 theories/lebesgue_measure.v
 theories/lebesgue_stieltjes_measure.v
 theories/forms.v
@@ -50,15 +61,9 @@ theories/lebesgue_integral.v
 theories/ftc.v
 theories/hoelder.v
 theories/probability.v
-theories/signed.v
-theories/itv.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v
-theories/showcase/uniform_bigO.v
 theories/showcase/summability.v
-theories/altreals/xfinmap.v
-theories/altreals/discrete.v
-theories/altreals/realseq.v
-theories/altreals/realsum.v
-theories/altreals/distr.v
+analysis_stdlib/Rstruct_topology.v
+analysis_stdlib/showcase/uniform_bigO.v

altreals/Make

@@ -0,0 +1,14 @@
+-Q . mathcomp.altreals
+
+-arg -w -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
+
+altreals/xfinmap.v
+altreals/discrete.v
+altreals/realseq.v
+altreals/realsum.v
+altreals/distr.v

altreals/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

analysis_stdlib/Make

@@ -0,0 +1,11 @@
+-Q . mathcomp.analysis_stdlib
+
+-arg -w -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
+
+Rstruct_topology.v
+showcase/uniform_bigO.v

analysis_stdlib/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

reals/Make

@@ -0,0 +1,17 @@
+-Q . mathcomp.reals
+
+-arg -w -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
+
+constructive_ereal.v
+reals.v
+real_interval.v
+signed.v
+itv.v
+prodnormedzmodule.v
+nsatz_realtype.v
+all_reals.v

reals/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

reals/all_reals.v

@@ -0,0 +1,7 @@
+From mathcomp Require Export signed.
+From mathcomp Require Export itv.
+From mathcomp Require Export constructive_ereal.
+From mathcomp Require Export reals.
+From mathcomp Require Export real_interval.
+From mathcomp Require Export prodnormedzmodule.
+From mathcomp Require Export nsatz_realtype.

reals_stdlib/Make

@@ -0,0 +1,10 @@
+-Q . mathcomp.reals_stdlib
+
+-arg -w -arg -parsing
+-arg -w -arg +undeclared-scope
+-arg -w -arg +non-primitive-record
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
+
+Rstruct.v

reals_stdlib/Makefile

@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common

theories/Make

@@ -7,25 +7,18 @@
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -projection-no-head-constant
 
-constructive_ereal.v
 ereal.v
-reals.v
 landau.v
-Rstruct.v
-Rstruct_topology.v
 topology.v
 separation_axioms.v
 function_spaces.v
 cantor.v
-prodnormedzmodule.v
 normedtype.v
 realfun.v
 sequences.v
 exp.v
 trigo.v
-nsatz_realtype.v
 esum.v
-real_interval.v
 lebesgue_measure.v
 forms.v
 derive.v
@@ -36,16 +29,8 @@ ftc.v
 hoelder.v
 probability.v
 lebesgue_stieltjes_measure.v
-signed.v
-itv.v
 convex.v
 charge.v
 kernel.v
 all_analysis.v
-showcase/uniform_bigO.v
 showcase/summability.v
-altreals/xfinmap.v
-altreals/discrete.v
-altreals/realseq.v
-altreals/realsum.v
-altreals/distr.v

theories/all_analysis.v

@@ -1,9 +1,5 @@
-From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export ereal.
-From mathcomp Require Export reals.
 From mathcomp Require Export landau.
-From mathcomp Require Export Rstruct.
-From mathcomp Require Export Rstruct_topology.
 From mathcomp Require Export topology.
 From mathcomp Require Export function_spaces.
 From mathcomp Require Export cantor.
@@ -13,9 +9,7 @@ From mathcomp Require Export realfun.
 From mathcomp Require Export sequences.
 From mathcomp Require Export exp.
 From mathcomp Require Export trigo.
-From mathcomp Require Export nsatz_realtype.
 From mathcomp Require Export esum.
-From mathcomp Require Export real_interval.
 From mathcomp Require Export lebesgue_measure.
 From mathcomp Require Export forms.
 From mathcomp Require Export derive.
@@ -26,8 +20,6 @@ From mathcomp Require Export ftc.
 From mathcomp Require Export hoelder.
 From mathcomp Require Export probability.
 From mathcomp Require Export lebesgue_stieltjes_measure.
-From mathcomp Require Export signed.
-From mathcomp Require Export itv.
 From mathcomp Require Export convex.
 From mathcomp Require Export charge.
 From mathcomp Require Export kernel.