From 200c1a2321d97e6a3f6bb5995288195478d7056b Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 24 Jul 2026 07:58:19 +0200
Subject: [PATCH] Fix opam file

---
 coq-mathcomp-odd-order.opam | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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 <>" ]