From a784a85aa5f3c1c15467d4256d6f01836c2dcb77 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 4 Nov 2023 21:26:17 +0100 Subject: [PATCH] fix(released): coq-mathcomp {1.18.0, 2.1.0} don't build anymore with coq.dev --- .../coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.18.0/opam | 2 +- .../coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.1.0/opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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"} ]