From bd2926f542e8aead35e99ec40bfe5649345322a7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 9 Dec 2020 16:58:31 +0100
Subject: [PATCH] remove Coq 8.10 compat code

---
 tests/proofmode_ascii.ref   | 6 +++---
 tests/proofmode_ascii.v     | 1 -
 tests/proofmode_monpred.ref | 8 ++++----
 tests/proofmode_monpred.v   | 7 +------
 4 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/tests/proofmode_ascii.ref b/tests/proofmode_ascii.ref
index a8e890845..ca5a27603 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 a05c9a716..74451f504 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 ea6b33fb2..bca8ecb77 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 f90d0db21..3e8d41a80 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.
-- 
GitLab