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: [