diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 84cb0b75819b3c8efc34d4ea3fb4b7dd048e5ec7..2527765eb8654eeda68ca410abedc84be56dd762 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+(* FIXME: This file needs a 'Proof Using' hint, but the default we use
+   everywhere makes for lots of extra ssumptions. *)
 
 Record solution (F : cFunctor) := Solution {
   solution_car :> ofeT;
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index b52eca914f52c8557b4cb034513315b4dd50cf41..3f828a5d86683f1ce6004f1df48a8a91c99639dd 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,7 +1,8 @@
 From iris.prelude Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
-Set Default Proof Using "Type*".
+(* FIXME: This file needs a 'Proof Using' hint, but the default we use
+   everywhere makes for lots of extra ssumptions. *)
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.