diff --git a/tests/atomic.v b/tests/atomic.v
index 62e5e23342f7ba3a2721c7a0d3d600859c47d5d7..afc6e55bd92d73b0ed54b93d19d96eeecb0a7f5b 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -2,7 +2,7 @@ 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.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f353c853d128d6ca0b17a9731d6025a84d6aebfe..b0bb09df68d05267839ff444ff96abb93dd95b7c 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,7 @@ 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.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 6057efb1c269752444b301cbe90c1667d1e1141a..735c423a3c13d09ad32c6d0eb73a5d9242b3a331 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics intro_patterns.
-Set Ltac Backtrace.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index c2998995f07dfbf422dda6f7165ce573d29b2242..3bfbc2ee5943fdb4de3c5a491cf707f9384d3cf4 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,7 +1,7 @@
 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.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 
 Section base_logic_tests.
   Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 320355c44b423707d29249ccaa0dd52f2490c6b9..b76927b8bc63801c50fce53c1bdb2f1e1de7ce54 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
-Set Ltac Backtrace.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 
 Section tests.
   Context {I : biIndex} {PROP : sbi}.
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index d9dc2c4e83e42b3d7da1560de4ed2436599cb23f..34a0321987b2a0c7eeef46dbbe30bf595a038982 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics .
 From iris.si_logic Require Import bi.
-Set Ltac Backtrace.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
 
 Section si_logic_tests.
   Implicit Types P Q R : siProp.