diff --git a/Makefile.coq.local b/Makefile.coq.local
index 7865fe690c6339505596df0a644f2056202c383e..cdb0b65ca639c95466003ade8b05641cd873e3fc 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -5,6 +5,10 @@ real-all: $(if $(NO_TEST),,test)
 TESTFILES=$(wildcard tests/*.v)
 
 test: $(TESTFILES:.v=.vo)
+# Make sure everything imports the options.
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! fgrep -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi \
+	done
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
diff --git a/_CoqProject b/_CoqProject
index fe5e41c89d02a123411e27863ce7d8e609a87304..a90e9b51ecef2f8a9c7b7e00b91f9ec8950e68e3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,6 +2,7 @@
 # "Declare Scope" does not exist yet in 8.9.
 -arg -w -arg -undeclared-scope
 
+theories/options.v
 theories/base.v
 theories/tactics.v
 theories/option.v
diff --git a/theories/base.v b/theories/base.v
index 117172ef2bbeba5c185ed033c5678a8ea74cfaa0..603fe11a829333a84def3835562361a7a752ebe0 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -10,9 +10,9 @@ we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
 From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
-Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
+From stdpp Require Import options.
 
 (** This notation is necessary to prevent [length] from being printed
 as [strings.length] if strings.v is imported and later base.v. See
diff --git a/theories/binders.v b/theories/binders.v
index 35e01ff709f459175d15afa3259bf844130597ca..ce03ccd9a3ce67eb1df80d0a95557ff9a8e156d3 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -7,6 +7,10 @@ This library is used in various Iris developments, like heap-lang, LambdaRust,
 Iron, Fairis. *)
 From stdpp Require Export strings.
 From stdpp Require Import sets countable finite fin_maps.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
 
 Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
diff --git a/theories/boolset.v b/theories/boolset.v
index 0312b8683ad9ecf6817dafc155813d1859e00b74..8ffe38973ebad67ccd24de4b4642dda9462300d7 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -1,6 +1,6 @@
 (** This file implements boolsets as functions into Prop. *)
 From stdpp Require Export prelude.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record boolset (A : Type) : Type := BoolSet { boolset_car : A → bool }.
 Arguments BoolSet {_} _ : assert.
diff --git a/theories/coGset.v b/theories/coGset.v
index b8816667974f777580eddcb5716bd25f4c888da1..51cb1c52ccfff1855a5e49f8ea26e73a9dc80fd4 100644
--- a/theories/coGset.v
+++ b/theories/coGset.v
@@ -6,7 +6,10 @@ Note that [coGset positive] cannot represent all elements of [coPset]
 infinite sets that cannot be represented). *)
 From stdpp Require Export sets countable.
 From stdpp Require Import decidable finite gmap coPset.
-(* Set Default Proof Using "Type". *)
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
 
 Inductive coGset `{Countable A} :=
   | FinGSet (X : gset A)
@@ -149,13 +152,16 @@ Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
 Definition gset_to_coGset `{Countable A} : gset A → coGset A := FinGSet.
 
 Section to_gset.
-  Context `{Countable A, Infinite A}.
+  Context `{Countable A}.
+
+  Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
+  Proof. done. Qed.
+
+  Context `{Infinite A}.
 
   Lemma elem_of_coGset_to_gset (X : coGset A) x :
     set_finite X → x ∈ coGset_to_gset X ↔ x ∈ X.
   Proof. rewrite coGset_finite_spec. by destruct X. Qed.
-  Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
-  Proof. done. Qed.
   Lemma gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
   Proof. by rewrite coGset_finite_spec. Qed.
 End to_gset.
diff --git a/theories/coPset.v b/theories/coPset.v
index 1aefcbe5ee7ea6992a444aa80d1568f916973987..1a46079ba5c5c08eb2a072d46bd00eb2ac0182a8 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -11,7 +11,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
 to the decision function that map bitstrings to bools. *)
 From stdpp Require Export sets.
 From stdpp Require Import pmap gmap mapset.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Local Open Scope positive_scope.
 
 (** * The tree data structure *)
diff --git a/theories/countable.v b/theories/countable.v
index 1b70eeb28903e7c4b8f19d75b78120f11a1f3e10..5b368a332cfefd87d49af17d8effa7c1db34a729 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import QArith_base Qcanon.
 From stdpp Require Export list numbers list_numbers.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Local Open Scope positive.
 
 Class Countable A `{EqDecision A} := {
diff --git a/theories/decidable.v b/theories/decidable.v
index 01cd5d8cbe8e3c01deafa78d050d94602e702061..73d175990e8f7c3e821d62cdb5375dec6a021f2a 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -2,6 +2,9 @@
 with a decidable equality. Such propositions are collected by the [Decision]
 type class. *)
 From stdpp Require Export proof_irrel.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
 Lemma dec_stable `{Decision P} : ¬¬P → P.
diff --git a/theories/fin.v b/theories/fin.v
index ab26009904c28f300f310837027f936fcea33c02..dc99e703ef37af27505fc37ff958b81f15126945 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -3,7 +3,7 @@
 renames or changes their notations, so that it becomes more consistent with the
 naming conventions in this development. *)
 From stdpp Require Export base tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 (** * The fin type *)
 (** The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 886daae1785cc1af43d0e17f449558b58905a8c2..cd60364da715143e2e5e57606da67c5a2c5544d5 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -2,6 +2,9 @@
 maps. We provide such an axiomatization, instead of implementing the domain
 function in a generic way, to allow more efficient implementations. *)
 From stdpp Require Export sets fin_maps.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
 Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index db66a2495e086794f755f17683fb2b91cce09ef6..8861aea53b8afb2f32d93a92025f2067ebfc337b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -4,8 +4,11 @@ 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 fin_sets.
-(* FIXME: This file needs a 'Proof Using' hint, but the default we use
-   everywhere makes for lots of extra ssumptions. *)
+From stdpp Require Import options.
+
+(* FIXME: This file needs a 'Proof Using' hint, but they need to be set
+locally (or things moved out of sections) as no default works well enough. *)
+Unset Default Proof Using.
 
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 3778161516a669db75a657e0d673b42800e4439c..6473a4cb9761e8aaad9388df671ab84568b806b6 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -3,6 +3,9 @@ importantly, it implements a fold and size function and some useful induction
 principles on finite sets . *)
 From stdpp Require Import relations.
 From stdpp Require Export numbers sets.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
 (** Operations *)
diff --git a/theories/finite.v b/theories/finite.v
index 965debcc8d1f2e3f9f38e0d874038cd885fdf0c5..392075251b342707891cccbe75c07ee89f0001ec 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -1,5 +1,5 @@
 From stdpp Require Export countable vector.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Class Finite A `{EqDecision A} := {
   enum : list A;
diff --git a/theories/functions.v b/theories/functions.v
index 868a430b336e13894adca08da2b4b6c598c34159..1933044be613caa037676bb7e86172994b1aae55 100644
--- a/theories/functions.v
+++ b/theories/functions.v
@@ -1,5 +1,5 @@
 From stdpp Require Export base tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Section definitions.
   Context {A T : Type} `{EqDecision A}.
diff --git a/theories/gmap.v b/theories/gmap.v
index 46f27260d7a7a6f2ddc301f9b8a65448f60c3ce6..ada9e445041c1f81b93f2308dcc4f609c64909d3 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -11,7 +11,11 @@ To compute concrete results, you need to both:
 *)
 From stdpp Require Export countable infinite fin_maps fin_map_dom.
 From stdpp Require Import pmap mapset propset.
-(* Set Default Proof Using "Type". *)
+From stdpp Require Import options.
+
+(* FIXME: This file needs a 'Proof Using' hint, but they need to be set
+locally (or things moved out of sections) as no default works well enough. *)
+Unset Default Proof Using.
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index fda93e2ae8018f6a47c5fc35e02e76869527c08b..5729b0926aec6a148f985dcbe1c0eb39e34eeeaa 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -1,6 +1,6 @@
 From stdpp Require Export countable.
 From stdpp Require Import gmap.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
 Arguments GMultiSet {_ _ _} _ : assert.
diff --git a/theories/hashset.v b/theories/hashset.v
index 82bd138c0e2d73fe5152d769c2cd00066b9ec6b7..9588536abfb5a12e1ef405765132518ec3fecf96 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -3,7 +3,7 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary
 integer of type [Z], and contains an unordered list without duplicates. *)
 From stdpp Require Export fin_maps listset.
 From stdpp Require Import zmap.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record hashset {A} (hash : A → Z) := Hashset {
   hashset_car : Zmap (list A);
diff --git a/theories/hlist.v b/theories/hlist.v
index 1e0f9103706e8e98cd1f23e1cb93316fba753d31..86dbd4571f1ac31f5181eab64fadd4caebbb8cdf 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -1,5 +1,5 @@
 From stdpp Require Import tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Local Set Universe Polymorphism.
 
 (* Not using [list Type] in order to avoid universe inconsistencies *)
diff --git a/theories/infinite.v b/theories/infinite.v
index 841e9de2616c6307eff9ab64cc4995bcdab21d59..3ca0885127f295fcbf4c9dadb75055589e4fffe6 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -1,5 +1,9 @@
 From stdpp Require Export list.
 From stdpp Require Import relations pretty.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
 
 (** * Generic constructions *)
 (** If [A] is infinite, and there is an injection from [A] to [B], then [B] is
@@ -24,12 +28,15 @@ The construction then finds the first string starting with [s] followed by a
 number that's not in the input list. For example, given [["H", "H1", "H4"]] and
 [s := "H"], it would find ["H2"]. *)
 Section search_infinite.
-  Context {B} (f : nat → B) `{!Inj (=) (=) f, !EqDecision B}.
+  Context {B} (f : nat → B).
 
   Let R (xs : list B) (n1 n2 : nat) :=
     n2 < n1 ∧ (f (n1 - 1)) ∈ xs.
   Lemma search_infinite_step xs n : f n ∈ xs → R xs (1 + n) n.
   Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed.
+
+  Context `{!Inj (=) (=) f, !EqDecision B}.
+
   Lemma search_infinite_R_wf xs : wf (R xs).
   Proof.
     revert xs. assert (help : ∀ xs n n',
diff --git a/theories/lexico.v b/theories/lexico.v
index e2739efb58da4babad911b559b90510d37043554..7e9be13326487709d6c82ddb691b149c2a469af4 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -1,7 +1,7 @@
 (** This files defines a lexicographic order on various common data structures
 and proves that it is a partial order having a strong variant of trichotomy. *)
 From stdpp Require Import numbers.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Notation cast_trichotomy T :=
   match T with
diff --git a/theories/list.v b/theories/list.v
index a0fa9d54fa31af628895a78dbbcb1b3105fd62e0..cddaea303943bb1bf01963cb08335b20013b0e65 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2,6 +2,9 @@
 are not in the Coq standard library. *)
 From Coq Require Export Permutation.
 From stdpp Require Export numbers base option.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
 Arguments length {_} _ : assert.
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 7393cd62d748749a772e076bf162f51fa3158b8d..917b67ce51b7a9adc2291b8de4e2b4b8c761f070 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -1,7 +1,7 @@
 (** This file collects general purpose definitions and theorems on
 lists of numbers that are not in the Coq standard library. *)
 From stdpp Require Export list.
-Set Default Proof Using "Type*".
+From stdpp Require Import options.
 
 (** * Definitions *)
 (** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
diff --git a/theories/listset.v b/theories/listset.v
index 2e0e892cb663bcb2f98fed4402c8e8f9bf5c6b61..7c3a2f275a742f3945685e3b4ccad96794208314 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,7 +1,7 @@
 (** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
 From stdpp Require Export sets list.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record listset A := Listset { listset_car: list A }.
 Arguments listset_car {_} _ : assert.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index 9f9139ea76feb213c89c33f996a2c9c859d6a547..84dc7c519b49531244a2606b598fb5afd269ba19 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -2,7 +2,7 @@
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
 From stdpp Require Export sets list.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
diff --git a/theories/mapset.v b/theories/mapset.v
index 2e99898f11090ec86c77879df343db6b32ee9fdd..cee12c66f465e76d1d0a4d71b15122d3cb0cd42a 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -2,7 +2,11 @@
 elements of the unit type. Since maps enjoy extensional equality, the
 constructed finite sets do so as well. *)
 From stdpp Require Export countable fin_map_dom.
-(* FIXME: This file needs a 'Proof Using' hint. *)
+From stdpp Require Import options.
+
+(* FIXME: This file needs a 'Proof Using' hint, but they need to be set
+locally (or things moved out of sections) as no default works well enough. *)
+Unset Default Proof Using.
 
 Record mapset (M : Type → Type) : Type :=
   Mapset { mapset_car: M (unit : Type) }.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 12dc464c30dcb6ed410c8d9c228d4673d9fc2ef7..b68326b5720a52ee2e988daf40a1c01c231acbab 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -1,5 +1,5 @@
 From stdpp Require Export countable coPset.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Definition namespace := list positive.
 Instance namespace_eq_dec : EqDecision namespace := _.
diff --git a/theories/nat_cancel.v b/theories/nat_cancel.v
index d6dff3ace763e93eca963d36bc3609114bfb7bea..2ae1bfa48e8c18c9fe15f5da5b19f49d9e110ff8 100644
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
@@ -1,4 +1,5 @@
 From stdpp Require Import numbers.
+From stdpp Require Import options.
 
 (** The class [NatCancel m n m' n'] is a simple canceler for natural numbers
 implemented using type classes.
diff --git a/theories/natmap.v b/theories/natmap.v
index d53da944a3e85c2a4dd0ab80b9fa002e332fa966..8c92083726b6b9371cfd6813968da51449e83272 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -2,7 +2,7 @@
 over Coq's data type of unary natural numbers [nat]. The implementation equips
 a list with a proof of canonicity. *)
 From stdpp Require Import fin_maps mapset.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Notation natmap_raw A := (list (option A)).
 Definition natmap_wf {A} (l : natmap_raw A) :=
diff --git a/theories/nmap.v b/theories/nmap.v
index fdf9fab5e380cf52181741d667239c9d7ae9a681..5d0645bff13c3b1a4fb827beee21665114f742d0 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -2,7 +2,7 @@
 maps whose keys range over Coq's data type of binary naturals [N]. *)
 From stdpp Require Import pmap mapset.
 From stdpp Require Export prelude fin_maps.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Local Open Scope N_scope.
 
diff --git a/theories/numbers.v b/theories/numbers.v
index d1a2d1946e991a23b7a5ab31e57d6b3a495a13ae..644f04904f884b81573154f08c06e9cf5dd92741 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -4,7 +4,7 @@ notations. *)
 From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
 From stdpp Require Export base decidable option.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Local Open Scope nat_scope.
 
 Coercion Z.of_nat : nat >-> Z.
diff --git a/theories/option.v b/theories/option.v
index f8c284a9159a7554a62ad95d0b4cd400342fceb5..545c884b45e2d64eec4e511ded34c51a00e48b3c 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -1,7 +1,7 @@
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
 From stdpp Require Export tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
   | ReflectSome x : P x → option_reflect P Q (Some x)
diff --git a/theories/options.v b/theories/options.v
new file mode 100644
index 0000000000000000000000000000000000000000..7e3856858e2a8b84e9f61b0034e0de133151aee5
--- /dev/null
+++ b/theories/options.v
@@ -0,0 +1,14 @@
+(** Coq configuration for std++ (not meant to leak to clients) *)
+(* Everything here should be [Export Set], which means when this
+file is *imported*, the option will only apply on the import site
+but not transitively. *)
+
+Export Set Default Proof Using "Type".
+(* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
+Export Set Suggest Proof Using. *)
+Export Set Default Goal Selector "!".
+
+(* "Fake" import to whitelist this file for the check that ensures we import
+this file everywhere.
+From stdpp Require Import options.
+*)
diff --git a/theories/orders.v b/theories/orders.v
index 84527ab6058e96e70f54cd45b422c6b985c61934..a7be2aa8c0173148967484d89ecae0a2940bcf64 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -1,7 +1,7 @@
 (** Properties about arbitrary pre-, partial, and total orders. We do not use
 the relation [⊆] because we often have multiple orders on the same structure *)
 From stdpp Require Export tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Section orders.
   Context {A} {R : relation A}.
diff --git a/theories/pmap.v b/theories/pmap.v
index 3f507bd7d7d341f5455ae29ed55de59674d02079..d89ef60b3f0e5f77cedf9c7bb492bf6aff2525a6 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -8,7 +8,7 @@ Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
 From stdpp Require Import mapset countable.
 From stdpp Require Export fin_maps.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Local Open Scope positive_scope.
 Local Hint Extern 0 (_ =@{positive} _) => congruence : core.
diff --git a/theories/prelude.v b/theories/prelude.v
index 6e96b3f0c1d201dfe7cd733a60f75ab13eca2bab..9c18d5eef37d92341f80527275841733a676c2b2 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -12,3 +12,4 @@ From stdpp Require Export
   list
   list_numbers
   lexico.
+From stdpp Require Import options.
diff --git a/theories/pretty.v b/theories/pretty.v
index 296cccb22ab543f74fcef44fae7651358da98e41..ac5eb6ba380e6bc9e957833cc9d0c97a7528bf73 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -1,7 +1,7 @@
 From stdpp Require Export strings.
 From stdpp Require Import relations numbers.
 From Coq Require Import Ascii.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Class Pretty A := pretty : A → string.
 Definition pretty_N_char (x : N) : ascii :=
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 084176516357f0a527359b09014bc62d5bcb6c26..e1d3ebd9b029fa8dc4828dfbcbe75f03b4294c06 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -1,6 +1,6 @@
 (** This file collects facts on proof irrelevant types/propositions. *)
 From stdpp Require Export base.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
 
diff --git a/theories/propset.v b/theories/propset.v
index 9e29a4e73c1bca738b095779e7743527bdc58fd2..84367c5691d1e6eb9cb63fa24d5d779d96836094 100644
--- a/theories/propset.v
+++ b/theories/propset.v
@@ -1,6 +1,6 @@
 (** This file implements sets as functions into Prop. *)
 From stdpp Require Export sets.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record propset (A : Type) : Type := PropSet { propset_car : A → Prop }.
 Add Printing Constructor propset.
diff --git a/theories/relations.v b/theories/relations.v
index e4543886bb2a7c002850714d24de130f8bdb4cd3..5668bcc4c07501e969fbc267a05fca00f3cc9eb9 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -3,7 +3,7 @@ These are particularly useful as we define the operational semantics as a
 small step semantics. *)
 From Coq Require Import Wf_nat.
 From stdpp Require Export sets.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 (** * Definitions *)
 Section definitions.
diff --git a/theories/sets.v b/theories/sets.v
index 8cc2192b2422e019184f4c827135c2ddfd2f39a4..2f53d4d75788e44240039f657d99a726f8ebc4e5 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -2,8 +2,11 @@
 importantly, it implements some tactics to automatically solve goals involving
 sets. *)
 From stdpp Require Export orders list list_numbers.
-(* FIXME: This file needs a 'Proof Using' hint, but the default we use
-   everywhere makes for lots of extra ssumptions. *)
+From stdpp Require Import options.
+
+(* FIXME: This file needs a 'Proof Using' hint, but they need to be set
+locally (or things moved out of sections) as no default works well enough. *)
+Unset Default Proof Using.
 
 (* Higher precedence to make sure these instances are not used for other types
 with an [ElemOf] instance, such as lists. *)
diff --git a/theories/sorting.v b/theories/sorting.v
index 1ff4d45f9f7481e86a79102940e506c6c742d992..3f019e54d0e6902b2a0de8d23074b656831b0621 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -2,7 +2,7 @@
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
 From stdpp Require Export orders list.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Section merge_sort.
   Context {A} (R : relation A) `{∀ x y, Decision (R x y)}.
diff --git a/theories/streams.v b/theories/streams.v
index b1811214d0783819c801f1d5079417ca12c91904..7022bfba05ea262e5ec78b742fca3d24aae0384f 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -1,5 +1,5 @@
 From stdpp Require Export tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
 Arguments scons {_} _ _ : assert.
diff --git a/theories/stringmap.v b/theories/stringmap.v
index 4b601d83b0180181ea9b51ca333acfa37372a247..2f2d8e6a1158ff1a76b4fb421a7c71a7de89c4c9 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -4,7 +4,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap]
 and guarantees logarithmic-time operations. *)
 From stdpp Require Export fin_maps pretty.
 From stdpp Require Import gmap.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Notation stringmap := (gmap string).
 Notation stringset := (gset string).
diff --git a/theories/strings.v b/theories/strings.v
index a9f2bcc535f3bcdb87833ddf0e7f0b71ca19c7a3..0e694d549062089ec6a301632d3705a47728829b 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -2,7 +2,7 @@ From Coq Require Import Ascii.
 From Coq Require Export String.
 From stdpp Require Export list.
 From stdpp Require Import countable.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 (* To avoid randomly ending up with String.length because this module is
 imported hereditarily somewhere. *)
diff --git a/theories/tactics.v b/theories/tactics.v
index e3cb1f962b5dfd4f243a08ff0be62f82a5027850..781b59a9cb125cbf6dff02c3e117146748e53db9 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -3,7 +3,7 @@ the development. *)
 From Coq Require Import Omega.
 From Coq Require Export Lia.
 From stdpp Require Export decidable.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
 Proof. intros ->; reflexivity. Qed.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index b78eff49538e9cf773571d472c8a1dc8b28f9273..6582ccc86cf93e5bf31eeea6d0cbf8d07d8f37ca 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -1,5 +1,5 @@
 From stdpp Require Import base tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Local Set Universe Polymorphism.
 
diff --git a/theories/vector.v b/theories/vector.v
index 534d3fbc9d7a1141cd0133bdb14a9fda0c236a2d..d64538e839f4f0ae2214462c2650b43932fe19f1 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -4,7 +4,7 @@ renames or changes their notations, so that it becomes more consistent with the
 naming conventions in this development. *)
 From stdpp Require Import countable.
 From stdpp Require Export fin list.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Open Scope vector_scope.
 
 (** The type [vec n] represents lists of consisting of exactly [n] elements.
diff --git a/theories/zmap.v b/theories/zmap.v
index 005284f66e45a8f8211afb9d11161051a6af20db..47190f8db6fde3235f95180873e281fa4272052b 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -2,7 +2,7 @@
 maps whose keys range over Coq's data type of binary naturals [Z]. *)
 From stdpp Require Import pmap mapset.
 From stdpp Require Export prelude fin_maps.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Local Open Scope Z_scope.
 
 Record Zmap (A : Type) : Type :=