diff --git a/coq-mathcomp-odd-order.opam b/coq-mathcomp-odd-order.opam
index 6d9133c..8a4595e 100644
--- a/coq-mathcomp-odd-order.opam
+++ b/coq-mathcomp-odd-order.opam
@@ -11,9 +11,8 @@ build: [
 ]
 install: [ make "install" ]
 depends: [
-  "ocaml"
+  "coq-core" { >= "9.1" }
   "coq-mathcomp-character" { (>= "2.4.0") | (= "dev") }
-  "coq" { >= "9.1" }
 ]
 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 <>" ]