Skip to content
Snippets Groups Projects
Commit a092506c authored by Ralf Jung's avatar Ralf Jung
Browse files

drop support for Coq 8.11

parent 7ccdfe0d
No related branches found
No related tags found
No related merge requests found
...@@ -50,11 +50,6 @@ build-coq.8.12.2: ...@@ -50,11 +50,6 @@ build-coq.8.12.2:
OPAM_PINS: "coq version 8.12.2" OPAM_PINS: "coq version 8.12.2"
DENY_WARNINGS: "1" 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 # Nightly job with a known-to-work Coq version
# (so failures must be caused by std++) # (so failures must be caused by std++)
build-stdpp.dev-coq.8.13.1: build-stdpp.dev-coq.8.13.1:
......
...@@ -5,6 +5,8 @@ lemma. ...@@ -5,6 +5,8 @@ lemma.
## Iris master ## Iris master
Coq 8.11 is no longer supported in this version of Iris.
**Changes in `algebra`:** **Changes in `algebra`:**
* Generalize the authorative elements of the `view`, `auth` and `gset_bij` * Generalize the authorative elements of the `view`, `auth` and `gset_bij`
......
...@@ -30,11 +30,13 @@ Importing Iris has some side effects as the library sets some global options. ...@@ -30,11 +30,13 @@ Importing Iris has some side effects as the library sets some global options.
This version is known to compile with: 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) - 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 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). [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 ### Working *with* Iris
......
...@@ -13,7 +13,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo ...@@ -13,7 +13,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
""" """
depends: [ depends: [
"coq" { (>= "8.11" & < "8.14~") | (= "dev") } "coq" { (>= "8.12" & < "8.14~") | (= "dev") }
"coq-stdpp" { (= "dev.2021-03-23.0.c1266011") | (= "dev") } "coq-stdpp" { (= "dev.2021-03-23.0.c1266011") | (= "dev") }
] ]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment