diff --git a/Makefile.coq.local b/Makefile.coq.local
index fe6320aa2352ea6c7bba3207fcd9c49bb97d3c9b..9ceafe4c78e77fadbe75be6184269b6b1619b6eb 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -9,7 +9,7 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8)\b" -q && echo 1)
+COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\b" -q && echo 1)
 COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
diff --git a/tests/atomic.ref b/tests/atomic.ref
index e1099c9c8af10cf4c4f3bf7dd5b645466e2d6556..ba5c5ad608616ab2992086c7e9411483ad6fe03e 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -15,12 +15,8 @@
 "non_laterable"
      : string
 The command has indeed failed with message:
-Ltac call to "iAuIntro" failed.
 Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 The command has indeed failed with message:
-In nested Ltac calls to "awp_apply (open_constr)",
-"<ssreflect_plugin::ssrtclseq@0> wp_apply_core lem fun H => iApplyHyp H ; last  iAuIntro" and
-"iAuIntro", last call failed.
 Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 "printing"
      : string
diff --git a/tests/atomic.v b/tests/atomic.v
index afc6e55bd92d73b0ed54b93d19d96eeecb0a7f5b..125a261c18bfaa41ae9246fa617025aa02104174 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Export lifting notation.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index ac83b6d40d0301db200c115e332c6793333cf286..8d19418d3e9f263a36b63e9848174f844e820406 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -75,7 +75,6 @@
 "wp_nonclosed_value"
      : string
 The command has indeed failed with message:
-Ltac call to "wp_pure (open_constr)" failed.
 Tactic failure: wp_pure: cannot find ?y in (Var "x") or 
 ?y is not a redex.
 1 subgoal
@@ -175,6 +174,5 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
 "not_cmpxchg"
      : string
 The command has indeed failed with message:
-Ltac call to "wp_cmpxchg_suc" failed.
 Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in 
 (#() #()).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 8cc493fd75bb55ba835d2c7b1f1f2ab639793578..942b4bb794c1ab97bf940242a8aedd079fce1f22 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/list_reverse.8.9.ref b/tests/list_reverse.8.9.ref
deleted file mode 100644
index 2c8d900777a7f2ae8771cc1234c9f6b5a14ac975..0000000000000000000000000000000000000000
--- a/tests/list_reverse.8.9.ref
+++ /dev/null
@@ -1,33 +0,0 @@
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  hd, acc : val
-  xs, ys : list val
-  Φ : val → iPropI Σ
-  ============================
-  "Hxs" : is_list hd xs
-  "Hys" : is_list acc ys
-  "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
-  --------------------------------------∗
-  WP (rev hd) acc [{ v, Φ v }]
-  
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  acc : val
-  ys : list val
-  Φ : val → iPropI Σ
-  ============================
-  "Hys" : is_list acc ys
-  "HΦ" : ∀ w : val, is_list w ys -∗ Φ w
-  --------------------------------------∗
-  WP match: InjLV #() with
-       InjL <> => acc
-     | InjR "l" =>
-       let: "tmp1" := Fst ! "l" in
-       let: "tmp2" := Snd ! "l" in
-       "l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
-     end [{ v, Φ v }]
-  
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index be894c20a79851c59c2fd6be4b9de8ebab79c358..e45044a8275bdffdd30a5d1326d2afff652df913 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -78,50 +78,21 @@
   Q
   
 The command has indeed failed with message:
-Ltac call to "done" failed.
 No applicable tactic.
 The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr) as #",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)" and
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-last call failed.
 Tactic failure: iSpecialize: Q not persistent.
 "test_iAssert_intuitionistic"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first  done",
-"<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first  done",
-"iAssert (open_constr) with (constr) as (constr)",
-"iAssertCore (open_constr) with (constr) as (constr) (tactic3)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
 Tactic failure: iSpecialize: (|==> P)%I not persistent.
 The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
 Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
 P.
 The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
 Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
 "test_iNext_plus_3"
      : string
@@ -185,9 +156,6 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
 "test_iSimpl_in4"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iSimpl in (constr)",
-"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
-last call failed.
 Tactic failure: iEval: %: unsupported selection pattern.
 "test_iFrame_later_1"
      : string
@@ -210,9 +178,6 @@ Tactic failure: iEval: %: unsupported selection pattern.
   â–· emp
   
 The command has indeed failed with message:
-In nested Ltac calls to "iFrame (constr)",
-"<iris.proofmode.ltac_tactics.iFrame_go>" and
-"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
 Tactic failure: iFrame: cannot frame Q.
 "test_and_sep_affine_bi"
      : string
@@ -496,115 +461,71 @@ Tactic failure: iFrame: cannot frame Q.
 "iStopProof_not_proofmode"
      : string
 The command has indeed failed with message:
-Ltac call to "iStopProof" failed.
 Tactic failure: iStopProof: proofmode not started.
 "iAlways_spatial_non_empty"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iAlways", "iModIntro" and 
-"iModIntro (uconstr)", last call failed.
 Tactic failure: iModIntro: spatial context is non-empty.
 "iDestruct_bad_name"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic3)" and
-"iDestructCore (open_constr) as (constr) (tactic3)", last call failed.
 Tactic failure: iDestruct: "HQ" not found.
 "iIntros_dup_name"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
-"iIntro (constr)", last call failed.
 Tactic failure: iIntro: "HP" not fresh.
 The command has indeed failed with message:
-In nested Ltac calls to "iIntros ( (intropattern) )",
-"iIntro ( (intropattern) )" and "intros x", last call failed.
 x is already used.
 "iSplitL_one_of_many"
      : string
 The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
 Tactic failure: iSplitL: hypotheses ["HPx"] not found.
 The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
 Tactic failure: iSplitL: hypotheses ["HPx"] not found.
 "iSplitR_one_of_many"
      : string
 The command has indeed failed with message:
-Ltac call to "iSplitR (constr)" failed.
 Tactic failure: iSplitR: hypotheses ["HPx"] not found.
 The command has indeed failed with message:
-Ltac call to "iSplitR (constr)" failed.
 Tactic failure: iSplitR: hypotheses ["HPx"] not found.
 "iSplitL_non_splittable"
      : string
 The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
 Tactic failure: iSplitL: P not a separating conjunction.
 "iSplitR_non_splittable"
      : string
 The command has indeed failed with message:
-Ltac call to "iSplitR (constr)" failed.
 Tactic failure: iSplitR: P not a separating conjunction.
 "iCombine_fail"
      : string
 The command has indeed failed with message:
-Ltac call to "iCombine (constr) as (constr)" failed.
 Tactic failure: iCombine: hypotheses ["HP3"] not found.
 "iSpecialize_bad_name1_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
 Tactic failure: iSpecialize: "H" not found.
 "iSpecialize_bad_name2_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
 Tactic failure: iSpecialize: "H" not found.
 "iExact_fail"
      : string
 The command has indeed failed with message:
-Ltac call to "iExact (constr)" failed.
 Tactic failure: iExact: "HQ" not found.
 The command has indeed failed with message:
-Ltac call to "iExact (constr)" failed.
 Tactic failure: iExact: "HQ" : Q does not match goal.
 The command has indeed failed with message:
-Ltac call to "iExact (constr)" failed.
 Tactic failure: iExact: "HP"
 not absorbing and the remaining hypotheses not affine.
 "iClear_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HP" not found.
 The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)",
-"<iris.proofmode.ltac_tactics.iClear_go>" and
-"<iris.proofmode.ltac_tactics.iClearHyp>", last call failed.
 Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
 "iSpecializeArgs_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializeArgs (constr) (open_constr)",
-"<iris.proofmode.ltac_tactics.iSpecializeArgs_go>" and
-"notypeclasses refine (uconstr)", last call failed.
 In environment
 PROP : sbi
 P : PROP
@@ -612,173 +533,80 @@ The term "true" has type "bool" while it is expected to have type "nat".
 "iStartProof_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iStartProof" and "iStartProof", last call failed.
 Tactic failure: iStartProof: not a BI assertion.
 "iPoseProof_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (open_constr) as (tactic3)" and 
-"iIntoEmpValid", last call failed.
 Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
 The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
-fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
-"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
-"iRename (constr) into (constr)", last call failed.
 Tactic failure: iRename: "H" not fresh.
 "iPoseProof_not_found_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)" and
-"iPoseProofCoreHyp (constr) as (constr)", last call failed.
 Tactic failure: iPoseProof: "Hx" not found.
 "iPoseProof_not_found_fail2"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
-fun Htmp =>
-  lazymatch lem with
-  | {| itrm := _; itrm_vars := ?xs; itrm_hyps := ?pat |} => iSpecializeCore
-  {| itrm := Htmp; itrm_vars := xs; itrm_hyps := pat |} as p
-  | _ => idtac
-  end), "iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
 Tactic failure: iSpecialize: hypotheses ["HQ"] not found.
 "iPoseProofCoreHyp_not_found_fail"
      : string
 The command has indeed failed with message:
-Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
 Tactic failure: iPoseProof: "Hx" not found.
 "iPoseProofCoreHyp_not_fresh_fail"
      : string
 The command has indeed failed with message:
-Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
 Tactic failure: iPoseProof: "H1" not fresh.
 "iRevert_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iRevert (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "H" not found.
 "iDestruct_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)", 
-"tac" (bound to fun H => iDestructHyp H as pat),
-"iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>", last call failed.
 Tactic failure: iDestruct: "{HP}"
 should contain exactly one proper introduction pattern.
 The command has indeed failed with message:
-In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)", 
-"tac" (bound to fun H => iDestructHyp H as pat),
-"iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
-"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
 Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
 invalid.
 "iOrDestruct_fail"
      : string
 The command has indeed failed with message:
-Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
 Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
 The command has indeed failed with message:
-Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
 Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
 "iApply_fail"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)", 
-"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
-failed.
 Tactic failure: iApply: cannot apply P.
 "iApply_fail_not_affine_1"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)", 
-"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
-failed.
 Tactic failure: iApply: Q
 not absorbing and the remaining hypotheses not affine.
 "iApply_fail_not_affine_2"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)", 
-"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
-failed.
 Tactic failure: iApply: Q
 not absorbing and the remaining hypotheses not affine.
 "iRevert_wrong_var"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) )" and 
-"iForallRevert (ident)", last call failed.
 Tactic failure: iRevert: k1 not in scope.
 The command has indeed failed with message:
-In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
-"iLöbRevert (constr) with (tactic3)",
-"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
-"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
-"∗" with tac), "iRevertIntros (constr) with (tactic3)", 
-"iRevertIntros_go", "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as
-IH), "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
-"iRevertIntros ( (ident) ) (constr) with (tactic3)",
-"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
-"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )), 
-"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
-"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
 Tactic failure: iRevert: k1 not in scope.
 "iRevert_dup_var"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) (ident) )",
-"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
 Tactic failure: iRevert: k not in scope.
 "iRevert_dep_var_coq"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) )", "iForallRevert (ident)" and
-"revert (ne_var_list)", last call failed.
 k is used in hypothesis Hk.
 "iRevert_dep_var"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) )" and 
-"iForallRevert (ident)", last call failed.
 Tactic failure: iRevert: k is used in hypothesis "Hk".
 "iLöb_no_sbi"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iLöb as (constr)",
-"iLöbRevert (constr) with (tactic3)",
-"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
-"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
-"∗" with tac), "iRevertIntros (constr) with (tactic3)", 
-"iRevertIntros_go", "tac" (bound to iLöbCore as IH), 
-"tac" (bound to iLöbCore as IH) and "iLöbCore as (constr)", last call failed.
 Tactic failure: iLöb: not a step-indexed BI entailment.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index fc1e7df41d68ad0bb4bdb3f38cf5f4ca9d082344..93876587b5f7e4c67ede34e2a0e93094ebef2653 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,4 @@
 From iris.proofmode Require Import tactics intro_patterns.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 6ebe13d84e424d0fe758d1da03beb2b76a065c16..9cbbce1b7e71dea57196fe5676091208b0bb93e1 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -110,22 +110,10 @@
 "test_iInv_12"
      : string
 The command has indeed failed with message:
-In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic3)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
-failed.
 Tactic failure: iInv: selector 34 is not of the right type .
 The command has indeed failed with message:
-In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic3)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
-failed.
 Tactic failure: iInv: invariant nroot not found.
 The command has indeed failed with message:
-In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic3)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
-failed.
 Tactic failure: iInv: invariant "H2" not found.
 "test_iInv"
      : string
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 39fabcd8d975a48aba36e52c46bb26218faf3dad..3392c95dfae8029737703fc2a2320d6d2b9995b8 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,7 +1,6 @@
 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.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 
 Section base_logic_tests.
   Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 72d54d672894514f9517e13d8894a112866e7edd..973c967d95ffff9bad1dc6e1853814b5a83788aa 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -58,9 +58,6 @@
   ∀ _ : (), ∃ _ : (), emp
   
 The command has indeed failed with message:
-In nested Ltac calls to "iFrame (constr)",
-"<iris.proofmode.ltac_tactics.iFrame_go>" and
-"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
 Tactic failure: iFrame: cannot frame (P i).
 1 subgoal
   
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 268ffa905284ae031e869a28cc6de38d73130c92..a1b445dbbd9ddb3536fc32d6413147196dbe654c 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.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
 
 Section tests.
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index 34a0321987b2a0c7eeef46dbbe30bf595a038982..61d894ea426e4953fa039e2ba94431d67a080c63 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics .
 From iris.si_logic Require Import bi.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 
 Section si_logic_tests.
   Implicit Types P Q R : siProp.