Merge pull request #71 from coq-community/opam

Update opam files following removal of Stdlib dep
coq-community · Feb 25, 2025 · de7e174 · de7e174
2 parents b23e3a8 + add58b4
commit de7e174
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 6 deletions.
diff --git a/coq-fourcolor-reals.opam b/coq-fourcolor-reals.opam
@@ -15,9 +15,11 @@ with proofs of properties such as categoricity."""
 build: [make "-C" "theories/reals" "-j%{jobs}%"]
 install: [make "-C" "theories/reals" "install"]
 depends: [
-  "coq" {>= "8.18"}
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
   "coq-mathcomp-ssreflect" {>= "2.1.0"}
-  "coq-mathcomp-algebra" 
+  "coq-mathcomp-algebra"
+  "coq-hierarchy-builder" {>= "1.5.0"}
 ]
 
 tags: [

diff --git a/coq-fourcolor.opam b/coq-fourcolor.opam
@@ -17,10 +17,6 @@ basic plane topology definitions, and a theory of combinatorial hypermaps."""
 build: [make "-C" "theories/proof" "-j%{jobs}%"]
 install: [make "-C" "theories/proof" "install"]
 depends: [
-  "coq" {>= "8.18"}
-  "coq-mathcomp-ssreflect" {>= "2.1.0"}
-  "coq-mathcomp-algebra" 
-  "coq-hierarchy-builder" {>= "1.5.0"}
   "coq-fourcolor-reals" {= version}
 ]