diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index de16cf2cf253245ec1a32b4bd036f40863b011bd..5f157ca4284d73f28f30dac6c65b4e3e4c4284a0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -50,11 +50,6 @@ build-coq.8.12.2: OPAM_PINS: "coq version 8.12.2" DENY_WARNINGS: "1" -build-coq.8.11.2: - <<: *template - variables: - OPAM_PINS: "coq version 8.11.2" - # Nightly job with a known-to-work Coq version # (so failures must be caused by std++) build-stdpp.dev-coq.8.13.1: diff --git a/CHANGELOG.md b/CHANGELOG.md index 9ea121fed6d674abc9ecebe4595c7cc8aabf4d76..f07e719dce927af0b0296b4010a70a165c05b854 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,8 @@ lemma. ## Iris master +Coq 8.11 is no longer supported in this version of Iris. + **Changes in `algebra`:** * Generalize the authorative elements of the `view`, `auth` and `gset_bij` diff --git a/README.md b/README.md index 2f66f35615be2b08178da7eaaab49e5cb5550e9a..7808c83dbaf09eea211cc2b14e20ef30abdc20bd 100644 --- a/README.md +++ b/README.md @@ -30,11 +30,13 @@ Importing Iris has some side effects as the library sets some global options. This version is known to compile with: - - Coq 8.11.2 / 8.12.2 / 8.13.1 + - Coq 8.12.2 / 8.13.1 - A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp) If you need to work with Coq 8.9 or Coq 8.10, you can use the [iris-3.3 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.3). +For a version compatible with Coq 8.11, check out the +[iris-3.4 branch](https://gitlab.mpi-sws.org/iris/iris/tree/iris-3.4). ### Working *with* Iris diff --git a/coq-iris.opam b/coq-iris.opam index e515bee60cfbb3da1711589795a8a2ee96fd5979..1ff77cda0a00b78f20675dfe8aa9f215d8e3e072 100644 --- a/coq-iris.opam +++ b/coq-iris.opam @@ -13,7 +13,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo """ depends: [ - "coq" { (>= "8.11" & < "8.14~") | (= "dev") } + "coq" { (>= "8.12" & < "8.14~") | (= "dev") } "coq-stdpp" { (= "dev.2021-03-23.0.c1266011") | (= "dev") } ]