diff --git a/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam b/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam
index ac76d93f8..5238b2b16 100644
--- a/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam
+++ b/extra-dev/packages/rocq-mathcomp-real-closed/rocq-mathcomp-real-closed.dev/opam
@@ -17,7 +17,7 @@ order theory of real closed field, through quantifier elimination."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "rocq-core" {= "dev"}
+  "rocq-core" {>= "9.0"}
   "rocq-mathcomp-ssreflect" {>= "2.4"}
   "rocq-mathcomp-algebra" 
   "rocq-mathcomp-field"