diff --git a/iris/prelude/prelude.v b/iris/prelude/prelude.v
index 8c458361c768f9e0c7f926769bef73ed31f06d9b..cf8da5882697eaa9e920e9567b8c962ea48e4923 100644
--- a/iris/prelude/prelude.v
+++ b/iris/prelude/prelude.v
@@ -1,13 +1,5 @@
-From Coq.ssr Require Export ssreflect.
-From stdpp Require Export prelude.
+From stdpp Require Export ssreflect.
 From iris.prelude Require Import options.
-Global Open Scope general_if_scope.
-Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
-Ltac done := stdpp.tactics.done.
 
 (** Iris itself and many dependencies still rely on this coercion. *)
 Coercion Z.of_nat : nat >-> Z.
-
-(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
-fixed in Coq >= 8.12, which Iris depends on. *)
-Global Hint Mode Equiv ! : typeclass_instances.