diff --git a/theories/collections.v b/theories/collections.v
index 1a34474de8b500c426a104cc83b9d8e12d4ea8d7..e4856b525e9e067dce3da35af50a471c206f77de 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -4,7 +4,8 @@
 importantly, it implements some tactics to automatically solve goals involving
 collections. *)
 From stdpp 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/fin_maps.v b/theories/fin_maps.v
index cc85921f2f41792e5d4c8f6dd0b91d3d968f6764..89b5ebedb3898e4109fddb66e847fbbe3a2bd5f6 100644
--- a/theories/fin_maps.v
+++ b/theories/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 stdpp 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