Merge pull request #1906 from proux01/fix-opam

Fix opam files

Author: proux01

coq-mathcomp-analysis-stdlib.opam

@@ -7,17 +7,8 @@ dev-repo: "git+https://github.com/math-comp/analysis.git"
 bug-reports: "https://github.com/math-comp/analysis/issues"
 license: "CECILL-C"
 
-build: [make "-C" "analysis_stdlib" "-j%{jobs}%"]
-install: [make "-C" "analysis_stdlib" "install"]
 depends: [ "rocq-mathcomp-analysis-stdlib" { = version} ]
 
-tags: [
-  "category:Mathematics/Real Numbers"
-  "category:Mathematics/Real Calculus and Topology"
-  "keyword:real numbers"
-  "keyword:reals"
-  "logpath:mathcomp.reals_stdlib"
-]
 authors: [
   "Reynald Affeldt"
   "Alessandro Bruni"

coq-mathcomp-analysis.opam

@@ -7,33 +7,8 @@ dev-repo: "git+https://github.com/math-comp/analysis.git"
 bug-reports: "https://github.com/math-comp/analysis/issues"
 license: "CECILL-C"
 
-build: [make "-C" "theories" "-j%{jobs}%"]
-install: [make "-C" "theories" "install"]
 depends: [ "rocq-mathcomp-analysis" { = version} ]
 
-tags: [
-  "category:Mathematics/Real Calculus and Topology"
-  "keyword:analysis"
-  "keyword:Cantor"
-  "keyword:topology"
-  "keyword:real numbers"
-  "keyword:sequence"
-  "keyword:convexity"
-  "keyword:Landau notation"
-  "keyword:logarithm"
-  "keyword:sin"
-  "keyword:cos"
-  "keyword:tangent"
-  "keyword:trigonometric function"
-  "keyword:exponential"
-  "keyword:differentiation"
-  "keyword:derivative"
-  "keyword:measure theory"
-  "keyword:integration"
-  "keyword:Lebesgue"
-  "keyword:probability"
-  "logpath:mathcomp.analysis"
-]
 authors: [
   "Reynald Affeldt"
   "Alessandro Bruni"

coq-mathcomp-classical.opam

@@ -7,28 +7,11 @@ dev-repo: "git+https://github.com/math-comp/analysis.git"
 bug-reports: "https://github.com/math-comp/analysis/issues"
 license: "CECILL-C"
 
-build: [make "-C" "classical" "-j%{jobs}%"]
-install: [make "-C" "classical" "install"]
 depends: [
-  "coq-core" { (>= "9.0" & < "9.2~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
-  "coq-mathcomp-fingroup"
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-finmap" { (>= "2.1.0") }
-  "coq-hierarchy-builder" { (>= "1.8.0") }
+  "coq-core"
+  "rocq-mathcomp-classical" {= version}
 ]
 
-tags: [
-  "category:Mathematics/Logic/Classical logic"
-  "keyword:classical logic"
-  "keyword:logic"
-  "keyword:sets"
-  "keyword:set theory"
-  "keyword:function"
-  "keyword:cardinal"
-  "keyword:filter"
-  "logpath:mathcomp.classical"
-]
 authors: [
   "Reynald Affeldt"
   "Alessandro Bruni"

coq-mathcomp-experimental-reals.opam

@@ -7,16 +7,8 @@ dev-repo: "git+https://github.com/math-comp/analysis.git"
 bug-reports: "https://github.com/math-comp/analysis/issues"
 license: "CECILL-C"
 
-build: [make "-C" "experimental_reals" "-j%{jobs}%"]
-install: [make "-C" "experimental_reals" "install"]
 depends: [ "rocq-mathcomp-experimental-reals" { = version} ]
 
-tags: [
-  "category:Mathematics/Real Numbers"
-  "keyword:real numbers"
-  "keyword:reals"
-  "logpath:mathcomp.experimental_reals"
-]
 authors: [
   "Reynald Affeldt"
   "Alessandro Bruni"

coq-mathcomp-reals-stdlib.opam

@@ -7,16 +7,8 @@ dev-repo: "git+https://github.com/math-comp/analysis.git"
 bug-reports: "https://github.com/math-comp/analysis/issues"
 license: "CECILL-C"
 
-build: [make "-C" "reals_stdlib" "-j%{jobs}%"]
-install: [make "-C" "reals_stdlib" "install"]
 depends: [ "rocq-mathcomp-reals-stdlib" { = version} ]
 
-tags: [
-  "category:Mathematics/Real Numbers"
-  "keyword:real numbers"
-  "keyword:reals"
-  "logpath:mathcomp.reals_stdlib"
-]
 authors: [
   "Reynald Affeldt"
   "Alessandro Bruni"

coq-mathcomp-reals.opam

@@ -7,17 +7,8 @@ dev-repo: "git+https://github.com/math-comp/analysis.git"
 bug-reports: "https://github.com/math-comp/analysis/issues"
 license: "CECILL-C"
 
-build: [make "-C" "reals" "-j%{jobs}%"]
-install: [make "-C" "reals" "install"]
 depends: [ "rocq-mathcomp-reals" { = version} ]
 
-tags: [
-  "category:Mathematics/Real Numbers"
-  "keyword:real numbers"
-  "keyword:reals"
-  "keyword:extended real numbers"
-  "logpath:mathcomp.reals"
-]
 authors: [
   "Reynald Affeldt"
   "Alessandro Bruni"

rocq-mathcomp-classical.opam

@@ -15,8 +15,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  ("coq" {>= "8.20" & < "8.21~"}
-  | "rocq-core" { (>= "9.0" & < "9.2~") | (= "dev") })
+  "rocq-core" { (>= "9.0" & < "9.2~") | (= "dev") }
   "rocq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
   "rocq-mathcomp-fingroup"
   "rocq-mathcomp-algebra"