diff --git a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.18.0/opam b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.18.0/opam index 35fe751b0b..bbbae920eb 100644 --- a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.18.0/opam +++ b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.18.0/opam @@ -8,7 +8,7 @@ license: "CECILL-B" build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ] install: [ make "-C" "mathcomp/ssreflect" "install" ] -depends: [ "coq" { ((>= "8.16" & < "8.19~") | (= "dev"))} ] +depends: [ "coq" {>= "8.16" & < "8.19~"} ] tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.ssreflect" ] authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] diff --git a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.1.0/opam b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.1.0/opam index 2bf79c9b32..2a75089218 100644 --- a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.1.0/opam +++ b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.1.0/opam @@ -11,7 +11,7 @@ install: [ make "-C" "mathcomp/ssreflect" "install" ] depends: [ ( ( "coq" {>= "8.16" & < "8.17~"} & "elpi" {>= "1.16.5"} ) | # The line above can be removed at the time support for 8.16 is dropped - ( "coq" { ((>= "8.16" & < "8.19~") | (= "dev"))} + ( "coq" {>= "8.16" & < "8.19~"} & "elpi" {>= "1.17.0"} ) ) "coq-hierarchy-builder" { >= "1.5.0"} ]