diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index aeff0bb..fa046ae 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,8 +17,6 @@ jobs: strategy: matrix: image: - - 'coqorg/coq:8.8' - - 'coqorg/coq:8.9' - 'coqorg/coq:8.10' - 'coqorg/coq:8.11' - 'coqorg/coq:8.12' diff --git a/README.md b/README.md index d80ead6..fa89449 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,7 @@ library. - Author(s): - Cyril Cohen - License: [CeCILL-B](LICENSE) -- Compatible Coq versions: 8.8 or later +- Compatible Coq versions: 8.10 or later - Additional dependencies: - [MathComp ssreflect](https://math-comp.github.io) 1.6 or later - Coq namespace: `mathcomp.bigenough` diff --git a/coq-mathcomp-bigenough.opam b/coq-mathcomp-bigenough.opam index 1f6af63..c26c70d 100644 --- a/coq-mathcomp-bigenough.opam +++ b/coq-mathcomp-bigenough.opam @@ -21,7 +21,7 @@ library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.8" & < "8.15~") | (= "dev")} + "coq" {(>= "8.10" & < "8.15~") | (= "dev")} "coq-mathcomp-ssreflect" {>= "1.6"} ] diff --git a/meta.yml b/meta.yml index 259829b..1afb2fe 100644 --- a/meta.yml +++ b/meta.yml @@ -34,8 +34,8 @@ license: identifier: CeCILL-B supported_coq_versions: - text: '8.8 or later' - opam: '{(>= "8.8" & < "8.15~") | (= "dev")}' + text: '8.10 or later' + opam: '{(>= "8.10" & < "8.15~") | (= "dev")}' dependencies: - opam: @@ -45,8 +45,6 @@ dependencies: [MathComp ssreflect](https://math-comp.github.io) 1.6 or later tested_coq_opam_versions: -- version: '8.8' -- version: '8.9' - version: '8.10' - version: '8.11' - version: '8.12' diff --git a/opam b/opam deleted file mode 100644 index 356722c..0000000 --- a/opam +++ /dev/null @@ -1,17 +0,0 @@ -opam-version: "1.2" -name: "coq-mathcomp-bigenough" -version: "1.0.0" -maintainer: "Cyril Cohen " - -homepage: "https://github.com/math-comp/bigenough" -bug-reports: "https://github.com/math-comp/bigenough/issues" -license: "CeCILL-B" -dev-repo: "https://github.com/math-comp/bigenough" - -build: [ make "-j" "%{jobs}%" ] -install: [ make "install" ] -remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/bigenough'" ] -depends: [ "coq-mathcomp-ssreflect" { (>= "1.6.0" | = "dev") } ] - -tags: [ "keyword:bigenough" "keyword:asymptotic reasoning" "keyword:small scale reflection" "keyword:mathematical components" ] -authors: [ "Cyril Cohen " ]