Rename altreals to experimental-reals

.nix/config.nix

@@ -3,7 +3,7 @@ let
     mathcomp-classical.job = true;
     mathcomp-reals.job = true;
     mathcomp-analysis.job = true;
-    mathcomp-altreals.job = true;
+    mathcomp-experimental-reals.job = true;
     mathcomp-reals-stdlib.job = true;
     mathcomp-analysis-stdlib.job = true;
     ssprove.job = false;

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"37d20f7c53fc3ee7de52eece3f0f23044ec32546"
+"7ff53c990ee876ed8aa55361cbf30a163702a13d"

CHANGELOG_UNRELEASED.md

@@ -20,7 +20,7 @@
 - in file `separation_axioms.v`,
   + new lemmas `compact_normal_local`, and `compact_normal`.
 
-- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals`
+- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals`
   with files
   + `xfinmap.v`
   + `discrete.v`

MANIFEST

@@ -10,18 +10,42 @@ NIX.md
 Licence_CeCILL-C_V1-en.txt
 
 # Build and meta data 
+reals_stdlib/Make
+reals_stdlib/Makefile
+analysis_stdlib/Make
+analysis_stdlib/Makefile
+classical/Make
+classical/Makefile
+Makefile.common
+experimental_reals/Make
+experimental_reals/Makefile
+theories/Make
+theories/Makefile
+reals/Make
+reals/Makefile
 Makefile
 Makefile.common
 _CoqProject
 .gitignore
 .travis.yml
-opam
-shell.nix
+coq-mathcomp-analysis-stdlib.opam
+coq-mathcomp-analysis.opam
+coq-mathcomp-classical.opam
+coq-mathcomp-experimental-reals.opam
+coq-mathcomp-reals-stdlib.opam
+coq-mathcomp-reals.opam
+default.nix
 
 # Theory files
+analysis_stdlib/*.v
+analysis_stdlib/showcase/*.v
+classical/*.v
+experimental_reals/*.v
+reals/*.v
+reals_stdlib/*.v
 theories/*.v
-theories/altreals/*.v
-theories/misc/*.v
+theories/showcase/*.v
+theories/topology_theory/*.v
 
 # Build scripts
 scripts/install-sh

_CoqProject

@@ -1,7 +1,7 @@
 -Q classical mathcomp.classical
 -Q reals mathcomp.reals
 -Q reals_stdlib mathcomp.reals_stdlib
--Q altreals mathcomp.altreals
+-Q experimental_reals mathcomp.experimental_reals
 -Q theories mathcomp.analysis
 -Q analysis_stdlib mathcomp.analysis_stdlib
 
@@ -32,11 +32,11 @@ 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
+experimental_reals/xfinmap.v
+experimental_reals/discrete.v
+experimental_reals/realseq.v
+experimental_reals/realsum.v
+experimental_reals/distr.v
 reals_stdlib/Rstruct.v
 theories/all_analysis.v
 theories/landau.v

coq-mathcomp-analysis-stdlib.opam

@@ -9,7 +9,7 @@ license: "CECILL-C"
 
 synopsis: "A library to link real numbers from mathematical components and Stdlib"
 description: """
-This repository contains a library to link real numbers for
+This package contains a library to link real numbers for
 the Coq proof-assistant using the Mathematical Components library and Stdlib."""
 
 build: [make "-C" "analysis_stdlib" "-j%{jobs}%"]

coq-mathcomp-analysis.opam

@@ -9,7 +9,7 @@ license: "CECILL-C"
 
 synopsis: "An analysis library for mathematical components"
 description: """
-This repository contains an experimental library for real analysis for
+This package contains a library for real analysis for
 the Coq proof-assistant and using the Mathematical Components library."""
 
 build: [make "-C" "theories" "-j%{jobs}%"]
@@ -24,8 +24,6 @@ depends: [
 tags: [
   "category:Mathematics/Real Calculus and Topology"
   "keyword:analysis"
-  "keyword:extended real numbers"
-  "keyword:filter"
   "keyword:Cantor"
   "keyword:topology"
   "keyword:real numbers"

coq-mathcomp-classical.opam

@@ -31,6 +31,7 @@ tags: [
   "keyword:set theory"
   "keyword:function"
   "keyword:cardinal"
+  "keyword:filter"
   "logpath:mathcomp.classical"
 ]
 authors: [

coq-mathcomp-altreals.opam → coq-mathcomp-experimental-reals.opam

@@ -9,11 +9,14 @@ license: "CECILL-C"
 
 synopsis: "A library for alternative real numbers for mathematical components"
 description: """
-This repository contains a library for alternative real numbers for
-the Coq proof-assistant and using the Mathematical Components library."""
+This package contains an experiment along real numbers
+made at the beginning of the MathComp-Analysis library
+(which now offers the coq-mathcomp-reals package).
 
-build: [make "-C" "altreals" "-j%{jobs}%"]
-install: [make "-C" "altreals" "install"]
+Beware that this still contains a few Admitted."""
+
+build: [make "-C" "experimental_reals" "-j%{jobs}%"]
+install: [make "-C" "experimental_reals" "install"]
 depends: [
   "coq-mathcomp-reals" { = version}
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
@@ -23,7 +26,7 @@ tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
   "keyword:reals"
-  "logpath:mathcomp.altreals"
+  "logpath:mathcomp.experimental_reals"
 ]
 authors: [
   "Reynald Affeldt"

coq-mathcomp-reals-stdlib.opam

@@ -9,7 +9,7 @@ license: "CECILL-C"
 
 synopsis: "A library to link real numbers from mathematical components and Stdlib"
 description: """
-This repository contains a library to link real numbers for
+This package contains a library to link real numbers for
 the Coq proof-assistant using the Mathematical Components library and Stdlib."""
 
 build: [make "-C" "reals_stdlib" "-j%{jobs}%"]

coq-mathcomp-reals.opam

@@ -9,7 +9,7 @@ license: "CECILL-C"
 
 synopsis: "A library for real numbers for mathematical components"
 description: """
-This repository contains a library for real numbers for
+This package contains a library for real numbers for
 the Coq proof-assistant and using the Mathematical Components library."""
 
 build: [make "-C" "reals" "-j%{jobs}%"]
@@ -22,6 +22,7 @@ tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
   "keyword:reals"
+  "keyword:extended real numbers"
   "logpath:mathcomp.reals"
 ]
 authors: [

altreals/Make → experimental_reals/Make

@@ -1,4 +1,4 @@
--Q . mathcomp.altreals
+-Q . mathcomp.experimental_reals
 
 -arg -w -arg -parsing
 -arg -w -arg +undeclared-scope