[extra-dev] Rename mathcomp-altreals to mathcomp-experimental-reals

coq · Nov 8, 2024 · b6022c7 · b6022c7
1 parent e6147f3
commit b6022c7
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 13 deletions.
diff --git a/extra-dev/packages/coq-mathcomp-analysis-stdlib/coq-mathcomp-analysis-stdlib.dev/opam b/extra-dev/packages/coq-mathcomp-analysis-stdlib/coq-mathcomp-analysis-stdlib.dev/opam
@@ -8,7 +8,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}%"]

diff --git a/extra-dev/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.dev/opam b/extra-dev/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.dev/opam
@@ -8,7 +8,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}%"]
@@ -23,8 +23,6 @@ depends: [
 tags: [
   "category:Mathematics/Real Calculus and Topology"
   "keyword:analysis"
-  "keyword:extended real numbers"
-  "keyword:filter"
   "keyword:Cantor"
   "keyword:topology"
   "keyword:real numbers"

diff --git a/extra-dev/packages/coq-mathcomp-classical/coq-mathcomp-classical.dev/opam b/extra-dev/packages/coq-mathcomp-classical/coq-mathcomp-classical.dev/opam
@@ -23,17 +23,19 @@ depends: [
 ]
 
 tags: [
-  "category:Mathematics/Logic/Classical logic"
-  "keyword:classical logic"
+  "category:Mathematics/Classical Logic"
+  "keyword:classical"
   "keyword:logic"
   "keyword:sets"
   "keyword:set theory"
   "keyword:function"
   "keyword:cardinal"
+  "keyword:filter"
   "logpath:mathcomp.classical"
 ]
 authors: [
   "Reynald Affeldt"
+  "Alessandro Bruni"
   "Yves Bertot"
   "Cyril Cohen"
   "Marie Kerjean"

diff --git a/...p-altreals/coq-mathcomp-altreals.dev/opam → .../coq-mathcomp-experimental-reals.dev/opam b/...p-altreals/coq-mathcomp-altreals.dev/opam → .../coq-mathcomp-experimental-reals.dev/opam
@@ -8,11 +8,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") }
@@ -22,7 +25,7 @@ tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
   "keyword:reals"
-  "logpath:mathcomp.altreals"
+  "logpath:mathcomp.experimental_reals"
 ]
 authors: [
   "Reynald Affeldt"

diff --git a/extra-dev/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.dev/opam b/extra-dev/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.dev/opam
@@ -8,7 +8,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}%"]

diff --git a/extra-dev/packages/coq-mathcomp-reals/coq-mathcomp-reals.dev/opam b/extra-dev/packages/coq-mathcomp-reals/coq-mathcomp-reals.dev/opam
@@ -8,7 +8,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}%"]
@@ -21,6 +21,7 @@ tags: [
   "category:Mathematics/Real Numbers"
   "keyword:real numbers"
   "keyword:reals"
+  "keyword:extended real numbers"
   "logpath:mathcomp.reals"
 ]
 authors: [