diff --git a/Makefile.coq.local b/Makefile.coq.local
index f10e32d0231670eb1d872607f6f2e5ec1d665107..4d618052e7d1263a5c2301e0e812d6b50c0bc25e 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -12,6 +12,10 @@ TESTFILES:=$(wildcard tests/*.v)
 NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
+# Make sure everything imports the options.
+	$(HIDE)for FILE in $$(find theories/ -name "*.v" | fgrep -v theories/options.v); do \
+	  if ! fgrep -q 'From iris Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; exit 1; fi \
+	done
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index aa4b02911f8d9133da966fda7e268b2aafb68e64..901e4159ec444c1cd9a77db2c4df478abdef80b1 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -1,6 +1,6 @@
 From stdpp Require Export functions gmap gmultiset.
 From iris.algebra Require Export monoid.
-Set Default Proof Using "Type*".
+From iris Require Import options.
 Local Existing Instances monoid_ne monoid_assoc monoid_comm
   monoid_left_id monoid_right_id monoid_proper
   monoid_homomorphism_rel_po monoid_homomorphism_rel_proper
@@ -619,36 +619,36 @@ Section homomorphisms.
   Lemma big_opL_commute_L {A} (h : M1 → M2)
       `{!MonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
     h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
-  Proof. unfold_leibniz. by apply big_opL_commute. Qed.
+  Proof using Type*. unfold_leibniz. by apply big_opL_commute. Qed.
   Lemma big_opL_commute1_L {A} (h : M1 → M2)
       `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : nat → A → M1) l :
     l ≠ [] → h ([^o1 list] k↦x ∈ l, f k x) = ([^o2 list] k↦x ∈ l, h (f k x)).
-  Proof. unfold_leibniz. by apply big_opL_commute1. Qed.
+  Proof using Type*. unfold_leibniz. by apply big_opL_commute1. Qed.
 
   Lemma big_opM_commute_L `{Countable K} {A} (h : M1 → M2)
       `{!MonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
     h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
-  Proof. unfold_leibniz. by apply big_opM_commute. Qed.
+  Proof using Type*. unfold_leibniz. by apply big_opM_commute. Qed.
   Lemma big_opM_commute1_L `{Countable K} {A} (h : M1 → M2)
       `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : K → A → M1) m :
     m ≠ ∅ → h ([^o1 map] k↦x ∈ m, f k x) = ([^o2 map] k↦x ∈ m, h (f k x)).
-  Proof. unfold_leibniz. by apply big_opM_commute1. Qed.
+  Proof using Type*. unfold_leibniz. by apply big_opM_commute1. Qed.
 
   Lemma big_opS_commute_L `{Countable A} (h : M1 → M2)
       `{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
-  Proof. unfold_leibniz. by apply big_opS_commute. Qed.
+  Proof using Type*. unfold_leibniz. by apply big_opS_commute. Qed.
   Lemma big_opS_commute1_L `{ Countable A} (h : M1 → M2)
       `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     X ≠ ∅ → h ([^o1 set] x ∈ X, f x) = ([^o2 set] x ∈ X, h (f x)).
-  Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
+  Proof using Type*. intros. rewrite <-leibniz_equiv_iff. by apply big_opS_commute1. Qed.
 
   Lemma big_opMS_commute_L `{Countable A} (h : M1 → M2)
       `{!MonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
-  Proof. unfold_leibniz. by apply big_opMS_commute. Qed.
+  Proof using Type*. unfold_leibniz. by apply big_opMS_commute. Qed.
   Lemma big_opMS_commute1_L `{Countable A} (h : M1 → M2)
       `{!WeakMonoidHomomorphism o1 o2 (≡) h} (f : A → M1) X :
     X ≠ ∅ → h ([^o1 mset] x ∈ X, f x) = ([^o2 mset] x ∈ X, h (f x)).
-  Proof. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
+  Proof using Type*. intros. rewrite <-leibniz_equiv_iff. by apply big_opMS_commute1. Qed.
 End homomorphisms.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index caae9ed56adbf301b4c65865410373e5793355c5..edce5cb70dfb3ac99db7c5ee89b4de6bfbc15c70 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap gmultiset.
 From iris.algebra Require Export big_op cmra.
-Set Default Proof Using "Type*".
+From iris Require Import options.
 
 (** Option *)
 Lemma big_opL_None {M : cmraT} {A} (f : nat → A → option M) l :
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index baed9dd5b55e5481c7c7ef70bc322a0a14a393f2..9a086658334337a40602df2d94ea0f42488bb38d 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export auth excl updates.
 From iris.algebra Require Import local_updates.
 From iris.base_logic Require Import base_logic.
+From iris Require Import options.
 
 (** Authoritative CMRA where the fragment is exclusively owned.
 This is effectively a single "ghost variable" with two views, the frament [â—¯E a]
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 324de2eacc3627aa32348edf73874e1b519117c3..14cc4b58b031413a927ee81fb3dad58ebeda51a1 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export frac auth updates local_updates.
 From iris.algebra Require Import proofmode_classes.
+From iris Require Import options.
 
 (** Authoritative CMRA where the NON-authoritative parts can be fractional.
   This CMRA allows the original non-authoritative element [â—¯ a] to be split into
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index af7a5c07faf71310695462626944aa9fbfedede7..9020deebf2840e5f4e806da179310de71289eae1 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -19,6 +19,7 @@ difference:
 From Coq Require Import QArith Qcanon.
 From iris.algebra Require Export auth frac updates local_updates.
 From iris.algebra Require Import ufrac proofmode_classes.
+From iris Require Import options.
 
 Definition ufrac_authR (A : cmraT) : cmraT :=
   authR (optionUR (prodR ufracR A)).
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index e7443c7a22c87e1dce3ed3f50936e533c4771a10..b83e36f235fca6a718a5dbede17e0d43340ba827 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export cmra local_updates proofmode_classes.
+From iris Require Import options.
 
 (** ** Natural numbers with [add] as the operation. *)
 Section nat.
diff --git a/theories/algebra/proofmode_classes.v b/theories/algebra/proofmode_classes.v
index 2e42bebf536baed7bf351d42953d29b2596aa515..608b329e4e8bec79c5652dbe30ef26d821c70ec9 100644
--- a/theories/algebra/proofmode_classes.v
+++ b/theories/algebra/proofmode_classes.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.proofmode Require Export classes.
+From iris Require Import options.
 
 (* There are various versions of [IsOp] with different modes:
 
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 516274c0272a46e7dbfd3becb19cbd1e5d4d4114..593b6081f947ce2052138d82cf7c903871b2de33 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -1,5 +1,6 @@
 From iris.bi Require Export derived_connectives updates internal_eq plainly.
 From iris.base_logic Require Export upred.
+From iris Require Import options.
 Import uPred_primitive.
 
 (** BI instances for [uPred], and re-stating the remaining primitive laws in
diff --git a/theories/base_logic/bupd_alt.v b/theories/base_logic/bupd_alt.v
index 67d04dc7aa32c1736f9fe9aca047bf2c6aab87d4..b40031111a65e3f0ace2d9af73449eb8bf4588a9 100644
--- a/theories/base_logic/bupd_alt.v
+++ b/theories/base_logic/bupd_alt.v
@@ -1,5 +1,9 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export base_logic.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
 
 (** This file contains an alternative version of basic updates, that is
 expression in terms of just the plain modality [â– ]. *)
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index 80b52c855ec7b08ec24cd90fd05929855220c396..4d3654f6889fa2b3b2cb15c7f9d0deb8cd3eff2e 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -4,6 +4,9 @@ laws of the view shift. *)
 From stdpp Require Export coPset.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Export base_logic.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
 Section fupd.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index c5eba535ba9adb7204f53152895027ab453fa1c6..d9f3a0e981aa046d1a129e8aa7bbfe5b3ba1713a 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Export derived.
+From iris Require Import options.
 
 Import base_logic.bi.uPred.
 
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 0f955957782cf7e69bed088d0dead44669de592f..159f0b964a07c0fb761f84afc934f1f3048b1cee 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -1,5 +1,6 @@
 From iris.bi Require Import interface derived_connectives updates.
 From iris.algebra Require Export ofe.
+From iris Require Import options.
 
 Notation "P |- Q" := (P ⊢ Q)
   (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index 0ca78688d57be8f4091016ae3284c1bbb086f769..f75bddc201a24398327f9daad6738b01af1aacc6 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -1,5 +1,6 @@
 From iris.bi Require Export interface.
 From iris.algebra Require Import monoid.
+From iris Require Import options.
 
 Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
 Arguments bi_iff {_} _%I _%I : simpl never.
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 2a1bbc10712a197b65dbe99ec5c7ae5c02bd2e93..a9710b744658df236134877e46daa011045bc0d6 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1,5 +1,9 @@
 From iris.bi Require Export derived_connectives.
 From iris.algebra Require Import monoid.
+From iris Require Import options.
+
+(* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
 
 (** Naming schema for lemmas about modalities:
     M1_into_M2: M1 P ⊢ M2 P
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index b5c520709c6b4a69b901e8f00758f2cff70c8daa..06084c0be2d41a6ab1a7bf6abd5bc8f948916fac 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -1,5 +1,6 @@
 From iris.bi Require Export derived_laws.
 From iris.algebra Require Import monoid.
+From iris Require Import options.
 
 Module bi.
 Import interface.bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 9862bcd959f05e81187e958f753729ccb387388f..8a8374852ddc9e33aa3710498ec5d2477de9912e 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -1,6 +1,10 @@
 From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.algebra Require Import monoid.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
 
 Class Embed (A B : Type) := embed : A → B.
 Arguments embed {_ _ _} _%I : simpl never.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 25198a338f8e107f48c931e409a229abdfe4f769..b0df9c7573050e5e8485dcbe4f5e9dfd1c4d4170 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,5 +1,6 @@
 From iris.bi Require Export notation.
 From iris.algebra Require Export ofe.
+From iris Require Import options.
 Set Primitive Projections.
 
 Section bi_mixin.
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index 6ecd8ec6f4a8cca9bd468c85124b177d36e471ee..3ffb1d71f4332e5eba60fdfde98813cf1226f948 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -1,4 +1,5 @@
 From iris.bi Require Import derived_laws_later big_op.
+From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** This file defines a type class for BIs with a notion of internal equality.
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 5f91cfe4fca6993856881c8d54f25401e62909f5..3297952f2904fecdb955cba33968b988b424d86c 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -1,5 +1,8 @@
 From iris.bi Require Export bi.
 From iris.proofmode Require Import tactics.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 196d32b1d1d1561521699a17567cf12c17ad954a..8935289d8f80aaf3a634e5756d268ac029e019d8 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export bi.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+From iris Require Import options.
 Import bi.
 
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
@@ -35,7 +35,7 @@ Section least.
   Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
   Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
-  Proof.
+  Proof using Type*.
     rewrite /bi_least_fixpoint /=. iIntros "HF" (Φ) "#Hincl".
     iApply "Hincl". iApply (bi_mono_pred _ Φ with "[#]"); last done.
     iIntros "!>" (y) "Hy". iApply ("Hy" with "[# //]").
@@ -43,7 +43,7 @@ Section least.
 
   Lemma least_fixpoint_unfold_1 x :
     bi_least_fixpoint F x ⊢ F (bi_least_fixpoint F) x.
-  Proof.
+  Proof using Type*.
     iIntros "HF". iApply ("HF" $! (OfeMor (F (bi_least_fixpoint F))) with "[#]").
     iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#]"); last done.
     iIntros "!>" (z) "?". by iApply least_fixpoint_unfold_2.
@@ -51,7 +51,7 @@ Section least.
 
   Corollary least_fixpoint_unfold x :
     bi_least_fixpoint F x ≡ F (bi_least_fixpoint F) x.
-  Proof.
+  Proof using Type*.
     apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
   Qed.
 
@@ -64,7 +64,7 @@ Section least.
   Lemma least_fixpoint_strong_ind (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, F (λ x, Φ x ∧ bi_least_fixpoint F x) y -∗ Φ y) -∗
     ∀ x, bi_least_fixpoint F x -∗ Φ x.
-  Proof.
+  Proof using Type*.
     trans (∀ x, bi_least_fixpoint F x -∗ Φ x ∧ bi_least_fixpoint F x)%I.
     { iIntros "#HΦ". iApply (least_fixpoint_ind with "[]"); first solve_proper.
       iIntros "!>" (y) "H". iSplit; first by iApply "HΦ".
@@ -97,7 +97,7 @@ Section greatest.
 
   Lemma greatest_fixpoint_unfold_1 x :
     bi_greatest_fixpoint F x ⊢ F (bi_greatest_fixpoint F) x.
-  Proof.
+  Proof using Type*.
     iDestruct 1 as (Φ) "[#Hincl HΦ]".
     iApply (bi_mono_pred Φ (bi_greatest_fixpoint F) with "[#]").
     - iIntros "!>" (y) "Hy". iExists Φ. auto.
@@ -106,7 +106,7 @@ Section greatest.
 
   Lemma greatest_fixpoint_unfold_2 x :
     F (bi_greatest_fixpoint F) x ⊢ bi_greatest_fixpoint F x.
-  Proof.
+  Proof using Type*.
     iIntros "HF". iExists (OfeMor (F (bi_greatest_fixpoint F))).
     iSplit; last done. iIntros "!>" (y) "Hy /=". iApply (bi_mono_pred with "[#] Hy").
     iIntros "!>" (z) "?". by iApply greatest_fixpoint_unfold_1.
@@ -114,7 +114,7 @@ Section greatest.
 
   Corollary greatest_fixpoint_unfold x :
     bi_greatest_fixpoint F x ≡ F (bi_greatest_fixpoint F) x.
-  Proof.
+  Proof using Type*.
     apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
   Qed.
 
diff --git a/theories/bi/lib/relations.v b/theories/bi/lib/relations.v
index a42b93d8bc7ab5079795291095fbf834420f64a6..11f5d6aa75d5e2b8d3b825d103691d909d7792e9 100644
--- a/theories/bi/lib/relations.v
+++ b/theories/bi/lib/relations.v
@@ -2,6 +2,10 @@
 its reflexive transitive closure. *)
 From iris.bi.lib Require Export fixpoint.
 From iris.proofmode Require Import tactics.
+From iris Require Import options.
+
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
 
 Definition bi_rtc_pre `{!BiInternalEq PROP}
     {A : ofeT} (R : A → A → PROP)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 7202ef3753e612b404fbd8b9f495a2601a06cda5..f5a13ea1733f7d69465865d9be22fa57e5024078 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -1,6 +1,6 @@
 From stdpp Require Import coPset.
 From iris.bi Require Import bi.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Definitions. *)
 Structure biIndex :=
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index d67cc7f8948db4340dd8db5c36071cccb6ad1f2a..bea7f6b417b49412d3a49eb7e09defa70a4af5cf 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -1,3 +1,4 @@
+From iris Require Import options.
 (** Just reserve the notation. *)
 
 (** * Turnstiles *)
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index b81fe05d1a1c468757758a2072dffc5082044b27..95a1dd5c826dc82aa14829ce3bd031801fcfb71c 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -1,7 +1,11 @@
 From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.algebra Require Import monoid.
+From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
+
 Class Plainly (A : Type) := plainly : A → A.
 Arguments plainly {A}%type_scope {_} _%I.
 Hint Mode Plainly ! : typeclass_instances.
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
index 9c934356e8bc22395c07ca0f04e9c323fc965e96..2bef8b0e78e131b20140a3b57642ac86d031419f 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -1,6 +1,6 @@
 From stdpp Require Export telescopes.
 From iris.bi Require Export bi.
-Set Default Proof Using "Type*".
+From iris Require Import options.
 Import bi.
 
 (* This cannot import the proofmode because it is imported by the proofmode! *)
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 9690d30af7ac1eadb9089a1d3a45c3fbdad672b7..5c87a174db178fd8d35f99fd002d80e505b015ba 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -1,7 +1,11 @@
 From stdpp Require Import coPset.
 From iris.bi Require Import interface derived_laws_later big_op plainly.
+From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
+Set Default Proof Using "Type*".
+
 (* We first define operational type classes for the notations, and then later
 bundle these operational type classes with the laws. *)
 Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index d6de4370c2a4a6ea5f86b0afbf25f4c91a2cfa6e..ee7181d5cdefbe4c500410a268f0e7a31a0c1760 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -1,6 +1,7 @@
 From stdpp Require Export coPset.
 From iris.bi Require Import interface derived_connectives.
 From iris.program_logic Require Import language.
+From iris Require Import options.
 
 Inductive stuckness := NotStuck | MaybeStuck.
 
diff --git a/theories/heap_lang/lib/clairvoyant_coin.v b/theories/heap_lang/lib/clairvoyant_coin.v
index a865289baead07a0b4a1eb17917f923d18480911..70673ad50872c46a134b9ae74d333e8cefcce568 100644
--- a/theories/heap_lang/lib/clairvoyant_coin.v
+++ b/theories/heap_lang/lib/clairvoyant_coin.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Export nondet_bool.
+From iris Require Import options.
 
 (** The clairvoyant coin predicts all the values that it will
 *non-deterministically* choose throughout the execution of the
diff --git a/theories/heap_lang/lib/lazy_coin.v b/theories/heap_lang/lib/lazy_coin.v
index b22c0707a2cd57826d614118d1cba0108b8c4bcc..315cc5f3f88f28ee9030e6db500407934d690b42 100644
--- a/theories/heap_lang/lib/lazy_coin.v
+++ b/theories/heap_lang/lib/lazy_coin.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Export nondet_bool.
+From iris Require Import options.
 
 Definition new_coin: val := λ: <>, (ref NONE, NewProph).
 
diff --git a/theories/heap_lang/lib/nondet_bool.v b/theories/heap_lang/lib/nondet_bool.v
index fcf7f6a03a030c776df4cd306578b1b376e4dc94..98aec67e0dd8f8ffad59782dca8f547316de6589 100644
--- a/theories/heap_lang/lib/nondet_bool.v
+++ b/theories/heap_lang/lib/nondet_bool.v
@@ -1,6 +1,7 @@
 From iris.base_logic Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
+From iris Require Import options.
 
 Definition nondet_bool : val :=
   λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".
diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
index 4f4df7d122ea161f19aec98e2e071dbc5b3f5cc9..146b3816aca6f39d7b4b56f5909e9c5d6b8a3041 100644
--- a/theories/heap_lang/locations.v
+++ b/theories/heap_lang/locations.v
@@ -1,5 +1,6 @@
 From stdpp Require Import countable numbers gmap.
 From iris.algebra Require Import base.
+From iris Require Import options.
 
 Record loc := { loc_car : Z }.
 
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 5ff1dcb674762b21046e552d9d0d8bdd819a9056..106a1242398fde8492313962bbae567fc9e56cb8 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -1,5 +1,6 @@
 From stdpp Require Import gmap.
 From iris.heap_lang Require Export lang.
+From iris Require Import options.
 
 (* This file contains some metatheory about the heap_lang language,
   which is not needed for verifying programs. *)
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index a568a68c3d439311fe78f73f39647cf508102985..4cfeef1bc4497d9e00bedd0bb33f58f5c842ce87 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Export adequacy.
 From iris.heap_lang Require Export lang notation tactics.
+From iris Require Import options.
 
 (** This file contains the proof that prophecies can be safely erased
 from programs. We erase a program by replacing prophecy identifiers
diff --git a/theories/proofmode/ident_name.v b/theories/proofmode/ident_name.v
index c79e67e81b893923a07b4ff0a1c16178b95fda7e..136493f1305ab4de09300b0d561ebd2035e47f9c 100644
--- a/theories/proofmode/ident_name.v
+++ b/theories/proofmode/ident_name.v
@@ -1,4 +1,5 @@
 From stdpp Require Import base.
+From iris Require Import options.
 
 (** [ident_name] is a way to remember an identifier within the binder of a
 (trivial) function, which can be constructed and retrieved with Ltac but is easy
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 909b7324ca6109b59dba7b8196a017b68eabe1ea..93983d9d9117b21ba6433ebb1faf8b1960c15102 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -1,6 +1,7 @@
 From iris.bi Require Export monpred.
 From iris.bi Require Import plainly.
 From iris.proofmode Require Import tactics modality_instances.
+From iris Require Import options.
 
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index c9d616778b9208c260a161160b1c5faeaae43375..c92ba206bd0ccaa7e8cf5201d298bc2a595931b4 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -1,5 +1,6 @@
 From iris.bi Require Import bi telescopes.
 From iris.proofmode Require Import base environments.
+From iris Require Import options.
 
 (** Called by all tactics to perform computation to lookup items in the
     context.  We avoid reducing anything user-visible here to make sure we
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 636885cb87bda5d3e9d7a1044becdd6924e41037..6fdca9b1e416ceb7bdb9f55fb2c72185b6675cda 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -5,3 +5,4 @@ From iris.proofmode Require Import class_instances class_instances_later
   class_instances_updates class_instances_embedding
   class_instances_plainly class_instances_internal_eq.
 From iris.proofmode Require Import frame_instances modality_instances.
+From iris Require Import options.
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index 8392463e45d68675637e09dc128175fcfa4386ef..d9cc4ae66a4a4c5ef2d824f0d3be2927efbdccf4 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -1,5 +1,6 @@
 From iris.bi Require Export bi.
 From iris.si_logic Require Export siprop.
+From iris Require Import options.
 Import siProp_primitive.
 
 (** BI instances for [siProp], and re-stating the remaining primitive laws in
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index 1ea1bde1fe2301efd5a6911d36369f4798379847..cddd8489805368ef7c9e875ea29498482585091c 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export ofe.
 From iris.bi Require Import notation.
+From iris Require Import options.
 
 (** The type [siProp] defines "plain" step-indexed propositions, on which we
 define the usual connectives of higher-order logic, and prove that these satisfy