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") }