Split boolp and classical_sets in a new analysis package

_CoqProject

@@ -1,46 +1,47 @@
--arg -w
--arg -parsing
+-R classical mathcomp.classical
+-R theories mathcomp.analysis
+
+-arg -w -arg -parsing
 -arg -w -arg +undeclared-scope
 -arg -w -arg +non-primitive-record
--arg -w -arg +undeclared-scope
 -arg -w -arg -ambiguous-paths
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -projection-no-head-constant
 
-theories/mathcomp_extra.v
-theories/boolp.v
-theories/ereal.v
-theories/reals.v
-theories/posnum.v
-theories/nngnum.v
+classical/boolp.v
+classical/classical_sets.v
+classical/cardinality.v
+classical/ereal.v
+classical/forms.v
+classical/fsbigop.v
+classical/functions.v
+classical/mathcomp_extra.v
+classical/nngnum.v
+classical/nsatz_realtype.v
+classical/posnum.v
+classical/prodnormedzmodule.v
+classical/reals.v
+classical/Rstruct.v
+classical/signed.v
+classical/all_classical.v
 theories/landau.v
-theories/classical_sets.v
 theories/Rstruct.v
 theories/topology.v
-theories/prodnormedzmodule.v
 theories/normedtype.v
 theories/realfun.v
 theories/sequences.v
 theories/exp.v
 theories/trigo.v
-theories/nsatz_realtype.v
-theories/cardinality.v
 theories/esum.v
-theories/fsbigop.v
 theories/set_interval.v
 theories/lebesgue_measure.v
-theories/forms.v
 theories/derive.v
 theories/measure.v
 theories/numfun.v
 theories/lebesgue_integral.v
 theories/summability.v
-theories/functions.v
-theories/signed.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v
 theories/altreals/realsum.v
 theories/altreals/distr.v
-
--R theories mathcomp.analysis

classical/Make

@@ -0,0 +1,25 @@
+-R . mathcomp.classical
+
+-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
+
+boolp.v
+classical_sets.v
+cardinality.v
+ereal.v
+forms.v
+fsbigop.v
+functions.v
+mathcomp_extra.v
+nngnum.v
+nsatz_realtype.v
+posnum.v
+prodnormedzmodule.v
+reals.v
+Rstruct.v
+signed.v
+all_classical.v

classical/Makefile

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