Skip to content

Commit

Permalink
Merge pull request #2802 from erikmd/mathcomp-vs-coq-dev
Browse files Browse the repository at this point in the history
fix: Mark coq-mathcomp < 2.1.0 not compatible with coq.dev
  • Loading branch information
proux01 authored Oct 26, 2023
2 parents 4ef8284 + c0825ef commit 9ec8111
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ license: "CECILL-B"

build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/ssreflect" "install" ]
depends: [ "coq" { ((>= "8.13" & < "8.19~") | (= "dev"))} ]
depends: [ "coq" { (>= "8.13" & < "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 <>" ]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ license: "CECILL-B"

build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/ssreflect" "install" ]
depends: [ "coq" { ((>= "8.15" & < "8.19~") | (= "dev"))} ]
depends: [ "coq" { (>= "8.15" & < "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 <>" ]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ license: "CECILL-B"
build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/ssreflect" "install" ]
depends: [
"coq" { ((>= "8.16" & < "8.19~") | (= "dev"))}
"coq" { (>= "8.16" & < "8.19~") }
"coq-hierarchy-builder" { >= "1.4.0"}
]

Expand Down

0 comments on commit 9ec8111

Please sign in to comment.