From 6db8eac50790519c7d33671d69d694cfaf12e525 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 20 Jun 2023 22:55:27 +0900
Subject: [PATCH] update opam files

---
 coq-mathcomp-analysis.opam  | 2 +-
 coq-mathcomp-classical.opam | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
index ca0fe8a5e..d5db657ae 100644
--- a/coq-mathcomp-analysis.opam
+++ b/coq-mathcomp-analysis.opam
@@ -19,7 +19,7 @@ build: [make "-C" "theories" "-j%{jobs}%"]
 install: [make "-C" "theories" "install"]
 depends: [
   "coq-mathcomp-classical" { = version}
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") | (= "dev") }
+  "coq-mathcomp-solvable" { (>= "2.0.0") | (= "dev") }
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
 ]
diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam
index df7a3f671..f93b98e9f 100644
--- a/coq-mathcomp-classical.opam
+++ b/coq-mathcomp-classical.opam
@@ -18,12 +18,12 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  "coq" { (>= "8.14" & < "8.18~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.17~") | (= "dev") }
+  "coq" { (>= "8.16" & < "8.18~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.0.0") | (= "dev") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
-  "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.2.0") }
+  "coq-mathcomp-finmap" { (>= "2.0.0") | (= "dev") }
+  "coq-hierarchy-builder" { (>= "1.4.0") }
 ]
 
 tags: [