diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index dd3928187a6a0ecb1cac32eb022eb118dd80ae40..41e84948d73841d2d7a1f7186fdc52768da86a64 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -198,4 +198,6 @@ Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
 Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed.
 End proof.
 
+SearchAbout _.
+
 Typeclasses Opaque barrier_ctx send recv.
diff --git a/theories/prelude/collections.v b/theories/prelude/collections.v
index 3f6b96a3c3e84630b61125b2bf27e5a6027d2ce7..8b3319ee385823657c4150ed12a87c4091dc58cc 100644
--- a/theories/prelude/collections.v
+++ b/theories/prelude/collections.v
@@ -4,7 +4,8 @@
 importantly, it implements some tactics to automatically solve goals involving
 collections. *)
 From iris.prelude Require Export orders list.
-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. *)
 
 Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
diff --git a/theories/prelude/fin_maps.v b/theories/prelude/fin_maps.v
index 486ce36cdd5ffefe8b566fffb245a3569c872cf2..aba8c7479b8660a6d51efafd1569992767c89e42 100644
--- a/theories/prelude/fin_maps.v
+++ b/theories/prelude/fin_maps.v
@@ -6,7 +6,8 @@ induction principles for finite maps and implements the tactic
 [simplify_map_eq] to simplify goals involving finite maps. *)
 From Coq Require Import Permutation.
 From iris.prelude Require Export relations orders vector.
-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. *)
 
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index e27cd15d50d75143e24f795fb42ffcf947f541c6..df02d3969ee7e6a885cdc7ae7aa87d9e12d25675 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,7 +1,8 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.proofmode Require Import tactics.
-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. *)
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.