diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index b76927b8bc63801c50fce53c1bdb2f1e1de7ce54..268ffa905284ae031e869a28cc6de38d73130c92 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,7 @@
 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.
   Context {I : biIndex} {PROP : sbi}.