Add a coq-mathcomp-reals package

Author: proux01

_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

theories/altreals/LICENSE altreals/LICENSEtheories/altreals/LICENSE renamed to altreals/LICENSE

@@ -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/Make

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