Merge pull request #3136 from pi8027/fix-real-closed-2.0.1

Fix the dependencies of coq-mathcomp-real-closed.2.0.1
coq · Aug 5, 2024 · 9198bb4 · 9198bb4
2 parents dc745c3 + 705aa84
commit 9198bb4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.1/opam b/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.1/opam
@@ -17,8 +17,8 @@ order theory of real closed field, through quantifier elimination."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.21~"}
-  "coq-mathcomp-ssreflect" {>= "2.0.0"}
+  "coq" {>= "8.17" & < "8.21~"}
+  "coq-mathcomp-ssreflect" {>= "2.1.0"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" {>= "1.0.0"}