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.