diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 22e846f04311e8a7cae58c2e6d3bf315f4f111af..d39314f0727df59f464b844c15b1d999f7ec4957 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -31,6 +31,7 @@ build-coq.dev:
   <<: *template
   variables:
     OPAM_PINS: "coq version dev"
+    MANGLE_NAMES: "1"
 
 build-coq.8.13.1:
   <<: *template
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 8fd7b000ea20e8c285078d1d91ecabb8f05b073f..da05cdfcbba867c79d5cf93d3a698dacdff67d31 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2948,13 +2948,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
     end in
   lazymatch type of select with
   | string =>
-     eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
+     notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
      [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
   | ident  =>
-     eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
+     notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
      [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
   | namespace =>
-     eapply @tac_inv_elim with (j:=H) (Pclose:=Pclose_pat);
+     notypeclasses refine (tac_inv_elim _ _ H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
      [ (by iAssumptionInv select) || fail "iInv: invariant" select "not found" |..]
   | _ => fail "iInv: selector" select "is not of the right type "
   end;
diff --git a/tests/atomic.v b/tests/atomic.v
index f9881ffcd85934e945e3837e5a13bf60770d41a2..00d34addeb86e0212741ea1a427cd6e9e23134b6 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -3,6 +3,8 @@ From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section tests.
   Context `{!heapG Σ} {aheap: atomic_heap Σ}.
   Import atomic_heap.notation.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4fd2570e8f5650c82e2aacbdfad9ff0f10c5629b..a05b855a233e2906283cd485d5c8076b3f2b894b 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lang adequacy proofmode notation.
 From iris.heap_lang Require Import lang.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section tests.
   Context `{!heapG Σ}.
   Implicit Types P Q : iProp Σ.
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 334732089d05f98a877f5ded545789a5d930a002..85b25b90be4b4f34f65ee5b0b525303b68ab4224 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section printing_tests.
   Context `{!heapG Σ}.
 
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index b1a5d2d6167432abba4bd0e5fb3a85ab00d84b20..9f2cc58424df35971260f7be5bb23812fa11cc9a 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -9,6 +9,8 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 (** The proofs from Section 3.1 *)
 Section demo.
   Context {M : ucmra}.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index ba12c859905dd3f19d95dd96c063f2a6537d4798..3ecdbbe082757f3447672285950b2ce11a38326d 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section list_reverse.
 Context `{!heapG Σ}.
 Implicit Types l : loc.
diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v
index bb9eb5b427352468334f8ac270d7ba63e01a49df..00a84f31f2a30d28bdb9869cb64f76097181d287 100644
--- a/tests/mosel_paper.v
+++ b/tests/mosel_paper.v
@@ -8,6 +8,8 @@ ICFP 2018 *)
 From iris.bi Require Import monpred.
 From iris.proofmode Require Import tactics monpred.
 
+Unset Mangle Names.
+
 Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
   P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
 Proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 59df90b7596d3333726de26427c80a90a5380db4..0f93ccabf3c022299caf3b963a2652fbe83d6ec5 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -10,6 +10,8 @@ Set Default Proof Using "Type".
 (** This is the introductory example from the "Iris from the Ground Up" journal
 paper. *)
 
+Unset Mangle Names.
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* tryset *) (λ: "n",
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 72d1e4dccaf6a824c37da4403fe6d9c668e08d85..4b858ca73b34bc6627e4d73cb3c630510a4fbaa7 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -10,6 +10,8 @@ Set Default Proof Using "Type".
 (** This is the introductory example from Ralf's PhD thesis.
 The difference to [one_shot] is that [set] asserts to be called only once. *)
 
+Unset Mangle Names.
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* set *) (λ: "n",
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c6bb9934c3eb07be97deb457370e4eea1d0ef7e6..bf5c427a0950f187e06067b529f81c7300109278 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,6 +1,8 @@
 From iris.proofmode Require Import tactics intro_patterns.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section tests.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index cab53ecec4176b001d1e7a9e27df9ca99f6f4add..ebc45c6e531002e58e6b8f62ba3e075652dd8c36 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
 From iris.bi Require Import ascii.
 
 Set Default Proof Using "Type".
+Unset Mangle Names.
 
 (* Remove this and the [Set Printing Raw Literals.] below once we require Coq
 8.14. *)
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 700ffde500e1181e5cf009467bc5f30b82872c5e..f88ea6e87be6ceb6deede51eaec6331a50a3f178 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -3,6 +3,8 @@ From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
+Unset Mangle Names.
+
 Section base_logic_tests.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 5b0cc65a3ffbedbe5386728875c8afb57b6daafa..6e69c5c88d99b63e30ca76bcc6423c47985911bf 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,8 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
 
+Unset Mangle Names.
+
 Section tests.
   Context {I : biIndex} {PROP : bi}.
   Local Notation monPred := (monPred I PROP).
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 897592b185c66ebcfe74a977f9d3c7454643a6be..ce3a0290bed7f37916962052dce8c9e86d350520 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -2,6 +2,8 @@ From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section basic_tests.
   Context {PROP : bi}.
   Implicit Types P Q R : PROP.