From 2beea379e92260d9cfcb5f07578df5cc6c0225af Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 25 Feb 2025 09:50:11 +0100
Subject: [PATCH] Update opam file following removal of Stdlib dep

---
 coq-mathcomp-real-closed.opam | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/coq-mathcomp-real-closed.opam b/coq-mathcomp-real-closed.opam
index 8d443a5..0d74661 100644
--- a/coq-mathcomp-real-closed.opam
+++ b/coq-mathcomp-real-closed.opam
@@ -21,7 +21,8 @@ order theory of real closed field, through quantifier elimination."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.18"}
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
   "coq-mathcomp-ssreflect" {>= "2.1"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field"