Merge pull request coq#2704 from erikmd/fix-mathcomp-dev

fix(coq-mathcomp-ssreflect.dev): Relax elpi constraint to allow coq.8.16
proux01 · Sep 5, 2023 · 85ea021 · 85ea021
2 parents 463eae0 + 4dfc44a
commit 85ea021
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam b/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam
@@ -10,9 +10,11 @@ license: "CeCILL-B"
 build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
 install: [ make "-C" "mathcomp/ssreflect" "install" ]
 depends: [
-  "coq" {>= "8.16"}
+  ( ( "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.17"}
+      & "elpi" {>= "1.17.0"} ) )
   "coq-hierarchy-builder" {>= "1.5.0"}
-  "elpi" {>= "1.17.0"}
 ]
 
 tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.ssreflect" ]