Add a coq-mathcomp-reals package

Author: proux01

_CoqProject

@@ -1,5 +1,8 @@
 -Q classical mathcomp.classical
+-Q reals mathcomp.reals
+-Q reals_stdlib mathcomp.reals_stdlib
 -Q theories mathcomp.analysis
+-Q analysis_stdlib mathcomp.analysis_stdlib
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
@@ -20,26 +23,33 @@ classical/fsbigop.v
 classical/set_interval.v
 classical/classical_orders.v
 classical/filter.v
+reals/constructive_ereal.v
+reals/real_interval.v
+reals/signed.v
+reals/itv.v
+reals/prodnormedzmodule.v
+reals/nsatz_realtype.v
+reals/all_reals.v
+reals/altreals/xfinmap.v
+reals/altreals/discrete.v
+reals/altreals/realseq.v
+reals/altreals/realsum.v
+reals/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 +60,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

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

theories/Rstruct_topology.v analysis_stdlib/Rstruct_topology.vtheories/Rstruct_topology.v renamed to analysis_stdlib/Rstruct_topology.v

@@ -0,0 +1,22 @@
+-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
+altreals/xfinmap.v
+altreals/discrete.v
+altreals/realseq.v
+altreals/realsum.v
+altreals/distr.v

theories/showcase/uniform_bigO.v analysis_stdlib/showcase/uniform_bigO.vtheories/showcase/uniform_bigO.v renamed to analysis_stdlib/showcase/uniform_bigO.v

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

reals/Make

@@ -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.