Merge branch 'ralf/no-coq-8.10' into 'master'

drop support for Coq 8.10

Closes #388

See merge request iris/iris!603

.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:

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`.

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

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") }
 ]
 

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

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}.

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
   ============================

tests/proofmode_monpred.v

 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.