From 37e03ceb5ab305a64ff5aa4e296cde7daa2b8185 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 16 Sep 2020 15:14:59 +0200
Subject: [PATCH] add options file

---
 Makefile.coq.local       |  4 ++++
 _CoqProject              |  1 +
 theories/base.v          |  2 +-
 theories/binders.v       |  4 ++++
 theories/boolset.v       |  2 +-
 theories/coGset.v        | 14 ++++++++++----
 theories/coPset.v        |  2 +-
 theories/countable.v     |  2 +-
 theories/decidable.v     |  3 +++
 theories/fin.v           |  2 +-
 theories/fin_map_dom.v   |  3 +++
 theories/fin_maps.v      |  7 +++++--
 theories/fin_sets.v      |  3 +++
 theories/finite.v        |  2 +-
 theories/functions.v     |  2 +-
 theories/gmap.v          |  6 +++++-
 theories/gmultiset.v     |  2 +-
 theories/hashset.v       |  2 +-
 theories/hlist.v         |  2 +-
 theories/infinite.v      |  9 ++++++++-
 theories/lexico.v        |  2 +-
 theories/list.v          |  3 +++
 theories/list_numbers.v  |  2 +-
 theories/listset.v       |  2 +-
 theories/listset_nodup.v |  2 +-
 theories/mapset.v        |  6 +++++-
 theories/namespaces.v    |  2 +-
 theories/nat_cancel.v    |  1 +
 theories/natmap.v        |  2 +-
 theories/nmap.v          |  2 +-
 theories/numbers.v       |  2 +-
 theories/option.v        |  2 +-
 theories/options.v       | 11 +++++++++++
 theories/orders.v        |  2 +-
 theories/pmap.v          |  2 +-
 theories/prelude.v       |  5 +++++
 theories/pretty.v        |  2 +-
 theories/proof_irrel.v   |  2 +-
 theories/propset.v       |  2 +-
 theories/relations.v     |  2 +-
 theories/sets.v          |  7 +++++--
 theories/sorting.v       |  2 +-
 theories/streams.v       |  2 +-
 theories/stringmap.v     |  2 +-
 theories/strings.v       |  2 +-
 theories/tactics.v       |  2 +-
 theories/telescopes.v    |  2 +-
 theories/vector.v        |  2 +-
 theories/zmap.v          |  2 +-
 49 files changed, 109 insertions(+), 44 deletions(-)
 create mode 100644 theories/options.v

diff --git a/Makefile.coq.local b/Makefile.coq.local
index 7865fe69..cdb0b65c 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 fe5e41c8..a90e9b51 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 117172ef..2c42f50f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -10,7 +10,7 @@ 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".
+From stdpp Require Import options.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
diff --git a/theories/binders.v b/theories/binders.v
index 35e01ff7..ce03ccd9 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 0312b868..8ffe3897 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 b8816667..51cb1c52 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 1aefcbe5..1a46079b 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 1b70eeb2..5b368a33 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 01cd5d8c..73d17599 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 ab260099..dc99e703 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 886daae1..cd60364d 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 db66a249..8861aea5 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 37781615..6473a4cb 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 965debcc..39207525 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 868a430b..1933044b 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 46f27260..ada9e445 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 fda93e2a..5729b092 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 82bd138c..9588536a 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 1e0f9103..86dbd457 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 841e9de2..3ca08851 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 e2739efb..7e9be133 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 a0fa9d54..cddaea30 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 7393cd62..917b67ce 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 2e0e892c..7c3a2f27 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 9f9139ea..84dc7c51 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 2e99898f..cee12c66 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 12dc464c..b68326b5 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 d6dff3ac..2ae1bfa4 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 d53da944..8c920837 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 fdf9fab5..5d0645bf 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 d1a2d194..644f0490 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 f8c284a9..545c884b 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 00000000..fa046af6
--- /dev/null
+++ b/theories/options.v
@@ -0,0 +1,11 @@
+(** 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".
+
+(* "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 84527ab6..a7be2aa8 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 3f507bd7..d89ef60b 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 6e96b3f0..aff80807 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -12,3 +12,8 @@ From stdpp Require Export
   list
   list_numbers
   lexico.
+
+(* "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/pretty.v b/theories/pretty.v
index 296cccb2..ac5eb6ba 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 08417651..e1d3ebd9 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 9e29a4e7..84367c56 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 e4543886..5668bcc4 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 8cc2192b..2f53d4d7 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 1ff4d45f..3f019e54 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 b1811214..7022bfba 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 4b601d83..2f2d8e6a 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 a9f2bcc5..0e694d54 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 e3cb1f96..781b59a9 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 b78eff49..6582ccc8 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 534d3fbc..d64538e8 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 005284f6..47190f8d 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 :=
-- 
GitLab