Renaming coq-mathcomp-altreals to experimental-reals

Following discussion during last mathcomp sharing days
math-comp · Nov 6, 2024 · 2bbe176 · 2bbe176
1 parent d26b17b
commit 2bbe176
Show file tree

Hide file tree

Showing 13 changed files with 12 additions and 12 deletions.
diff --git a/.nix/config.nix b/.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;

diff --git a/CHANGELOG_UNRELEASED.md b/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`

diff --git a/_CoqProject b/_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

diff --git a/coq-mathcomp-altreals.opam → coq-mathcomp-experimental-reals.opam b/coq-mathcomp-altreals.opam → coq-mathcomp-experimental-reals.opam
@@ -12,8 +12,8 @@ description: """
 This repository contains a library for alternative real numbers for
 the Coq proof-assistant and using the Mathematical Components library."""
 
-build: [make "-C" "altreals" "-j%{jobs}%"]
-install: [make "-C" "altreals" "install"]
+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 +23,7 @@ tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
   "keyword:reals"
-  "logpath:mathcomp.altreals"
+  "logpath:mathcomp.experimental_reals"
 ]
 authors: [
   "Reynald Affeldt"

diff --git a/altreals/LICENSE → experimental_reals/LICENSE b/altreals/LICENSE → experimental_reals/LICENSE
diff --git a/altreals/Make → experimental_reals/Make b/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

diff --git a/altreals/Makefile → experimental_reals/Makefile b/altreals/Makefile → experimental_reals/Makefile
diff --git a/altreals/dedekind.v → experimental_reals/dedekind.v b/altreals/dedekind.v → experimental_reals/dedekind.v
diff --git a/altreals/discrete.v → experimental_reals/discrete.v b/altreals/discrete.v → experimental_reals/discrete.v
diff --git a/altreals/distr.v → experimental_reals/distr.v b/altreals/distr.v → experimental_reals/distr.v
diff --git a/altreals/realseq.v → experimental_reals/realseq.v b/altreals/realseq.v → experimental_reals/realseq.v
diff --git a/altreals/realsum.v → experimental_reals/realsum.v b/altreals/realsum.v → experimental_reals/realsum.v
diff --git a/altreals/xfinmap.v → experimental_reals/xfinmap.v b/altreals/xfinmap.v → experimental_reals/xfinmap.v