From c41c0b6fa0bf2695da90e4011e5c4cf1fce7f059 Mon Sep 17 00:00:00 2001
From: Aleksandar Nanevski <aleks.nanevski@imdea.org>
Date: Mon, 5 May 2025 16:26:34 +0200
Subject: [PATCH] updating coq and mathcomp versions

---
 coq-htt-core.opam | 2 +-
 coq-htt.opam      | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/coq-htt-core.opam b/coq-htt-core.opam
index 8182418..b856b31 100644
--- a/coq-htt-core.opam
+++ b/coq-htt-core.opam
@@ -36,7 +36,7 @@ install: [make "-C" "htt" "install"]
 depends: [
   "dune" {>= "3.6"}
   "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }
diff --git a/coq-htt.opam b/coq-htt.opam
index 4265e46..bb0c93a 100644
--- a/coq-htt.opam
+++ b/coq-htt.opam
@@ -32,8 +32,8 @@ build: [make "-C" "examples" "-j%{jobs}%"]
 install: [make "-C" "examples" "install"]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.1.0" & < "2.2~") | (= "dev") }