From c5e8c6f061966f0df49f13a687b70ce009e84b56 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Mon, 3 Feb 2025 11:11:50 +0100
Subject: [PATCH] real-closed.2.0.2 compiles on Rocq 9.0+rc1

---
 .../coq-mathcomp-real-closed.2.0.2/opam                         | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.2/opam b/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.2/opam
index a83556c4e..658eed37c 100644
--- a/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.2/opam
+++ b/released/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.2.0.2/opam
@@ -17,7 +17,7 @@ order theory of real closed field, through quantifier elimination."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.17" & < "8.21~"}
+  "coq" {>= "8.17" & < "9.1~"}
   "coq-mathcomp-ssreflect" {>= "2.1.0" & < "2.4"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-field"