Merge pull request #3328 from proux01/multinomials-rocq9

multinomials.2.3.0 and real-closed.2.0.2 compile with Rocq 9.0+rc1
coq · Feb 3, 2025 · 72b2319 · 72b2319
2 parents feeb2e3 + c5e8c6f
commit 72b2319
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam b/released/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.2.3.0/opam
@@ -8,7 +8,7 @@ authors: ["Pierre-Yves Strub"]
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq"                    {(>= "8.16" & < "8.21~") | = "dev"}
+  "coq"                    {(>= "8.16" & < "9.1~") | = "dev"}
   "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.4~") | = "dev"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {(>= "1.0" & < "1.1~") | = "dev"}

diff --git a/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.2/opam b/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.2/opam
@@ -17,7 +17,7 @@ order theory of real closed field, through quantifier elimination."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.17" & < "8.21~"}
+  "coq" {>= "8.17" & < "9.1~"}
   "coq-mathcomp-ssreflect" {>= "2.1.0" & < "2.4"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-field"