Merge pull request #71 from proux01/opam

Update opam file following removal of Stdlib dep
math-comp · Feb 25, 2025 · 1235078 · 1235078
2 parents 0accab9 + 2beea37
commit 1235078
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/coq-mathcomp-real-closed.opam b/coq-mathcomp-real-closed.opam
@@ -21,7 +21,8 @@ order theory of real closed field, through quantifier elimination."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.18"}
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
   "coq-mathcomp-ssreflect" {>= "2.1"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field"