diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0e5c30934986c74666c16205c1f3a32457ef1936..a35e0442c25434ba4f0ced360645a8b6771f163c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -32,6 +32,11 @@ build-coq.dev:
variables:
OPAM_PINS: "coq version dev"
+build-coq.8.13.dev:
+ <<: *template
+ variables:
+ OPAM_PINS: "coq version 8.13.dev"
+
build-coq.8.12.1:
<<: *template
variables:
@@ -48,11 +53,6 @@ build-coq.8.11.2:
variables:
OPAM_PINS: "coq version 8.11.2"
-build-coq.8.10.2:
- <<: *template
- variables:
- OPAM_PINS: "coq version 8.10.2"
-
# Nightly job with a known-to-work Coq version
# (so failures must be caused by std++)
build-stdpp.dev-coq.8.12.1:
@@ -65,7 +65,7 @@ build-stdpp.dev-coq.8.12.1:
- schedules
- api
-# Nightly job with latest Coq branch
+# Nightly job with latest Coq beta branch
build-stdpp.dev-coq.8.13.dev:
<<: *template
variables:
diff --git a/CHANGELOG.md b/CHANGELOG.md
index b5c07acdb187253e26a3f0d7a32b08e10f49e11a..4fe9f93ba689a48603aa4550f871a257ba0f8bea 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,7 +5,7 @@ lemma.
## Iris master
-With this release, we dropped support for Coq 8.9.
+With this release, we dropped support for Coq 8.9 and Coq 8.10.
We also split Iris into multiple opam packages: `coq-iris` no longer contains
HeapLang, which is now in a separate package `coq-iris-heap-lang`.
diff --git a/README.md b/README.md
index 9d94251faf17bd4cf43b54a95cdd119cedab0d81..9518affd301b0e906d96fc43c7bedded22101ae2 100644
--- a/README.md
+++ b/README.md
@@ -30,7 +30,7 @@ Importing Iris has some side effects as the library sets some global options.
This version is known to compile with:
- - Coq 8.10.2 / 8.11.2 / 8.12.1
+ - Coq 8.11.2 / 8.12.1
- A development version of [std++](https://gitlab.mpi-sws.org/iris/stdpp)
If you need to work with Coq 8.7 or Coq 8.8, please check out the
diff --git a/coq-iris.opam b/coq-iris.opam
index bed4bfb727fce02ad277b9168d6bf049bd734219..c93763e655ea7d3854412303bb82427012400b3e 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.10.2" & < "8.14~") | (= "dev") }
+ "coq" { (>= "8.11" & < "8.14~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-11-11.2.6385b547") | (= "dev") }
]
diff --git a/tests/proofmode_ascii.ref b/tests/proofmode_ascii.ref
index a8e8908459210a766671210b0a42e37552e8cb29..ca5a2760305f617d2345996fd1967835570f188d 100644
--- a/tests/proofmode_ascii.ref
+++ b/tests/proofmode_ascii.ref
@@ -154,21 +154,21 @@ Tactic failure: iInv: invariant "H2" not found.
PROP : bi
============================
- forall (P : PROP) (_ : True), bi_entails P P
+ forall P (_ : True), bi_entails P P
"p2"
: string
1 subgoal
PROP : bi
============================
- forall P : PROP, and True (bi_entails P P)
+ forall P, and True (bi_entails P P)
"p3"
: string
1 subgoal
PROP : bi
============================
- ex (fun P : PROP => bi_entails P P)
+ ex (fun P => bi_entails P P)
"p4"
: string
1 subgoal
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index a05c9a71651d593291cc47484a3048df123c2182..74451f504f1e4d4afade7420a99d3b204b32ca4c 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -5,7 +5,6 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
From iris.bi Require Import ascii.
Set Default Proof Using "Type".
-Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
Section base_logic_tests.
Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index ea6b33fb27527a229500e3694b4aae8e7e92affd..bca8ecb7704378c8ed81bf3baaab93364edd37c3 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -29,17 +29,17 @@
Objective0 : Objective Q
ð“Ÿ, ð“ : PROP
============================
- "H2" : ∀ i : I, Q i
+ "H2" : ∀ i, Q i
"H3" : ð“Ÿ
"H4" : ð“
--------------------------------------∗
- ∀ i : I, 𓟠∗ ð“ ∗ Q i
+ ∀ i, 𓟠∗ ð“ ∗ Q i
1 subgoal
I : biIndex
PROP : bi
- FU0 : BiFUpd PROP * ()
+ FU : BiFUpd PROP
P, Q : monPred
i : I
============================
@@ -50,7 +50,7 @@
I : biIndex
PROP : bi
- FU0 : BiFUpd PROP * ()
+ FU : BiFUpd PROP
P : monPred
i : I
============================
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index f90d0db21115ccfa291236847d8d133566dcd076..3e8d41a8042d2ed291ce15625bc45f1ee674eab1 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,5 @@
From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants.
-Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
Section tests.
Context {I : biIndex} {PROP : bi}.
@@ -102,11 +101,7 @@ Section tests.
iAssumption.
Qed.
- (* This is a hack to avoid avoid coq bug #5735: sections variables ignore hint
- modes. So we assume the instances in a way that cannot be used by type
- class resolution, and then separately declare the instance as such. *)
- Context (FU0 : BiFUpd PROP * unit).
- Instance FU : BiFUpd PROP := fst FU0.
+ Context (FU : BiFUpd PROP).
Lemma test_apply_fupd_intro_mask E1 E2 P :
E2 ⊆ E1 → P -∗ |={E1,E2}=> |={E2,E1}=> P.