diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 3f828a5d86683f1ce6004f1df48a8a91c99639dd..b52eca914f52c8557b4cb034513315b4dd50cf41 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,8 +1,7 @@
 From iris.prelude Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
-(* FIXME: This file needs a 'Proof Using' hint, but the default we use
-   everywhere makes for lots of extra ssumptions. *)
+Set Default Proof Using "Type*".
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.