Merge pull request #3281 from palmskog/odd-order-2.2

coq-mathcomp-odd-order.2.0.0 doesn't work with MathComp 2.2.0 and later
coq · Jan 3, 2025 · a6c24ef · a6c24ef
2 parents 895ece1 + d82cbf4
commit a6c24ef
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.0.0/opam b/released/packages/coq-mathcomp-odd-order/coq-mathcomp-odd-order.2.0.0/opam
@@ -10,8 +10,7 @@ build: [
 ]
 install: [ make "install" ]
 depends: [
-  "ocaml"
-  "coq-mathcomp-character" { (>= "2.0.0") | (= "dev") }
+  "coq-mathcomp-character" {>= "2.0.0" & < "2.2.0"}
 ]
 tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ]
 authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]