Cyril: updating order using @pi8027 branch expriment/order of mathcomp

math-comp · Jun 13, 2019 · dd86e52 · dd86e52
1 parent 0c132ef
commit dd86e52
Show file tree

Hide file tree

Showing 5 changed files with 2,030 additions and 1,159 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -17,6 +17,10 @@ env:
   - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.7"
   - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.8"
   - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.9"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.7"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.8"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.9"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.10"
 #  - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-dev"
   - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7"
   - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8"

diff --git a/opam b/opam
@@ -12,11 +12,12 @@ build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/finmap'" ]
 depends: [
-  "coq-mathcomp-ssreflect" { (>= "1.8.0" & < "1.9.0~") | (= "dev")}
+  "coq" { (>= "8.7" & < "8.11~") }
+  "coq-mathcomp-ssreflect" { (>= "1.8.0" & < "1.10.0~") }
   "coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1.0~") }
 ]
 tags: [ "keyword:finmap" "keyword:finset" "keyword:multiset" "keyword:order"]
-authors: [ "Cyril Cohen <[email protected]>" ]
+authors: [ "Cyril Cohen <[email protected]>" "Kazuhiko Sakaguchi <[email protected]>" ]
 synopsis: "Finite sets, finite maps, finitely supported functions, orders"
 description: """
 This library is an extension of mathematical component in order to