diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e8044f68da732fec2079ab1ba60b8a7bdf74ce93..9148a3e2796c515f5a07b97ee9f882c8a7aae245 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -6,6 +6,7 @@ iris-coq8.6:
   script:
   # prepare
   - . build/opam-ci.sh coq 8.6 coq-mathcomp-ssreflect 1.6.1
+  - build/check-options.sh
   # build
   - 'time make -j8 TIMED=y 2>&1 | tee build-log.txt'
   - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
diff --git a/_CoqProject b/_CoqProject
index dbeb27192793aeb041d3f2ebe60e9ae02431656b..fed967afdb5208ebfaad93c3c3fa9113df136056 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,6 @@
 -Q theories iris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+theories/iris_options.v
 theories/algebra/cmra.v
 theories/algebra/cmra_big_op.v
 theories/algebra/cmra_tactics.v
diff --git a/awk.Makefile b/awk.Makefile
index 09ded0aa64f3a85ee4a55668d21ee17bb9a362f0..0ba40e7f0bab889ea0ba67c8155d1fbce90b0d29 100644
--- a/awk.Makefile
+++ b/awk.Makefile
@@ -9,6 +9,11 @@
 	PROJECT=PIECES[2];
 }
 
+# Set the missing variable VFILES0 so that .v files are installed.
+/^VOFILES0=/ {
+	print "VFILES0=$(patsubst theories/%,%,$(filter theories/%,$(VFILES)))"
+}
+
 # Patch the uninstall target to work properly, and to also uninstall stale files.
 # Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
 /^uninstall:/ {
diff --git a/build/check-options.sh b/build/check-options.sh
new file mode 100755
index 0000000000000000000000000000000000000000..3189a4ff9d982129017c7a31d3be44495c15d11c
--- /dev/null
+++ b/build/check-options.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+set -e
+
+for file in $(find -name "*.v"); do
+    if [ "$file" != "./theories/iris_options.v" ]; then
+        if ! fgrep "Load iris_options." "$file" >/dev/null; then
+            echo "iris_options are not being loaded in $file."
+            exit 1
+        fi
+    fi
+done
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index f0cd0c5bce2db23c5615ce6be3db152c52443d2f..1ca24f340fd9b91413b8418826971d5c6f9a63b6 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import base_logic.
+Load iris_options.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
@@ -217,7 +218,6 @@ Section list_theory.
 End list_theory.
 
 Section agree.
-Local Set Default Proof Using "Type".
 Context {A : ofeT}.
 
 Definition agree_list (x : agree A) := agree_car x :: agree_with x.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 5a976d77da10a6b38f73c973f471a99220ea73eb..65b6980cb4abf926910aaf570678424d3d6d5451 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export excl local_updates.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import classes.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
 Add Printing Constructor auth.
diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 06262f85016146a1e84bda7aabd214fa1a33f602..2f99c74f0ddf195e71bec73ed9b24b80bf597993 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,6 +1,10 @@
 From mathcomp Require Export ssreflect.
 From stdpp Require Export prelude.
-Set Default Proof Using "Type".
+Load iris_options.
+
+(* We set this globally because we consider it a bug that ssreflect
+   touches this at all. *)
 Global Set Bullet Behavior "Strict Subproofs".
+
 Global Open Scope general_if_scope.
 Ltac done := stdpp.tactics.done.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index ac3ce2352feb6134fba317ba4598128e803e320a..5f6eb93a69f95c44bc3944fb49b6ea1747e95048 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Class PCore (A : Type) := pcore : A → option A.
 Instance: Params (@pcore) 2.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index 206c3ac11af52b5e14249109239c8c3d5dd59884..f944c531fc42d20229198ba14e6eb50857dbdefe 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra list.
 From stdpp Require Import functions gmap gmultiset.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** The operator [ [⋅] Ps ] folds [⋅] over the list [Ps]. This operator is not a
 quantifier, so it binds strongly.
diff --git a/theories/algebra/cmra_tactics.v b/theories/algebra/cmra_tactics.v
index a0d123cc4bc092d54c0248e3a134f7bb56322022..d157180c986ad8ccacd1afc63efd336b316f9938 100644
--- a/theories/algebra/cmra_tactics.v
+++ b/theories/algebra/cmra_tactics.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import cmra_big_op.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** * Simple solver for validity and inclusion by reflection *)
 Module ra_reflection. Section ra_reflection.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 9939f63dd3afb43407127213ae4dfbcd3748da77..6d3f1ea2a1a88cb8dad9e4702a6509bcc3064b89 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From stdpp Require Export collections coPset.
-Set Default Proof Using "Type".
+Load iris_options.
 (** This is pretty much the same as algebra/gset, but I was not able to
 generalize the construction without breaking canonical structures. *)
 
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 0474eb3a8b2d9fdb32cb6695c2190976b04b3c0e..c551396d036e8273ee8c1c7eaab430f80a87f100 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Record solution (F : cFunctor) := Solution {
   solution_car :> ofeT;
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index fde21171bca57b53d3cee173d0fcdc6ed76f59af..80ecfdb9f9c58819d60b40477942a4bfcb10182f 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import local_updates.
-Set Default Proof Using "Type".
+Load iris_options.
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 3ff595195b3de5228a84d27217d1ae5ea511d319..3f3e2ce6494a911de7a684e7f345dbef0d3cdc4a 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import ofe cmra.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (* Old notation for backwards compatibility. *)
 
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index 496775226fbb9819c81a82b9a3a9c38bc897bf3e..2316b1ca568d67604acea7e58a00a3b8ca844f1f 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra updates.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 70b6e3a44b6fb0674284a29e449cabcdbc035425..8e42fb7f423a6c5437611019491a8bc7a116df76 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+Load iris_options.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index d00e7d9c4e75b0487e5abc9036b444d680fe5875..295a47c40c0878566fdd50d96b07fe2fd3f36d16 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Notation frac := Qp (only parsing).
 
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 479d20e2ce809fd1bc95d8901620f6ef5554ab9d..da7c58ff06f36ffdd980258b280ef6ce58b1c682 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
 From stdpp Require Export gmap.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Section cofe.
 Context `{Countable K} {A : ofeT}.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 5bf2cfd6595de41bfc201f5ddb55abecad848d24..3aa6351d2546ffdff9a6dd4efda69da16f4346ad 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From stdpp Require Export collections gmap mapset.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (* The union CMRA *)
 Section gset.
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index eec5599dc7724c8a8f30191a4ede07a6c3835839..523309dc54c361c17e1a86617e3049b1bff4854b 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From stdpp Require Import finite.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 3077f9dd5d4972844a1ff582cc3999661e35a18c..af47f3e3abf043d9f859cba1d1e5b08b9e4a9bf6 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -2,7 +2,7 @@ From iris.algebra Require Export cmra.
 From stdpp Require Export list.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Section cofe.
 Context {A : ofeT}.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 267ef18832b8e38779aeea946c3407da73a147bf..4a67502be927d4dcb7f3194d005083b67360d510 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** * Local updates *)
 Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index d3ebd8e71cb0cbf2877b6a719a1f05fb868a652f..719fbff391b67d09bc21f963a9ee1a81d0dd6f5c 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export base.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** This files defines (a shallow embedding of) the category of OFEs:
     Complete ordered families of equivalences. This is a cartesian closed
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index f4f5766e0458eb9c1ef3e9034bfac6d98c6d0a37..5d31fe51744629920312b60e6f2ea757cc4ee7a8 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,7 +1,7 @@
 From stdpp Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
-Set Default Proof Using "Type".
+Load iris_options.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 20bbe63b8851ca8584534ba7056efc3cdb3f9646..0ab1c6c5b89fa38fd1ad20d702e4b9848c60d616 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** * Frame preserving updates *)
 (* This quantifies over [option A] for the frame.  That is necessary to
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index 2ca6c9087dbc858b4eb04501840fd664755d4985..2340766f4eb8943b4f39e06125732e6104ea6d13 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -1,7 +1,7 @@
 From stdpp Require Export vector.
 From iris.algebra Require Export ofe.
 From iris.algebra Require Import list.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Section ofe.
   Context {A : ofeT}.
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 701ff8357f9f8c43d9e446f76024b94a6c0fc15f..c328a0c319063340b9ea39bca1829ae417900d34 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export derived.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Module Import uPred.
   Export upred.uPred.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index d998ef2d8e7e7523ec91212fbe0bb868fdde5db2..91f1da3d7348908dbb311c1bb39568d5ebf273ee 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export list cmra_big_op.
 From iris.base_logic Require Export base_logic.
 From stdpp Require Import gmap fin_collections gmultiset functions.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
diff --git a/theories/base_logic/deprecated.v b/theories/base_logic/deprecated.v
index 4d4995e42430015c9aef59d887d5b85cd64d472f..4f29c6c08290e98fb2be76dc950738d6b0aeca0e 100644
--- a/theories/base_logic/deprecated.v
+++ b/theories/base_logic/deprecated.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import primitive.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
 Notation "■ φ" := (uPred_pure φ%C%type)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index bb4f7fa2a29ae4f3ab469bef17cefc077a8b68d4..6ea3b2f0944a541120b40f19e8487beb0fcf2827 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export primitive.
-Set Default Proof Using "Type".
+Load iris_options.
 Import upred.uPred primitive.uPred.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 72977057e15071c01f38531eab068b873ffc400e..b85485f55a5ee5b0b6d7bff7f387e88279c3f3f7 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (* In this file we show that the bupd can be thought of a kind of
    step-indexed double-negation when our meta-logic is classical *)
diff --git a/theories/base_logic/hlist.v b/theories/base_logic/hlist.v
index a035aad0250498b6d64bc6af5fa8ab20772b0b00..fd70780b35c6baa89c2aa59572d905742465bc57 100644
--- a/theories/base_logic/hlist.v
+++ b/theories/base_logic/hlist.v
@@ -1,6 +1,6 @@
 From stdpp Require Export hlist.
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index d5638eeb0de494a271d9d4766bced126e40f33fe..46844c20892b31cf217ac1f70ad86cd4d2cd74ac 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -3,7 +3,7 @@ From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 0722ee82331455c7c85cf8da7d4ecec0cf1caa6c..e2087b5e38ce27f83e68daec199046ba116991f8 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import auth gmap agree.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (** The CMRAs we need. *)
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 451fb5b0e464ed5063b803fdffe93b032335cf3d..038392984275633e0e13a325a0554a55d4e8c8ef 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants fractional.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 4cf762d772d2c4519e702088fe58858dbd0eeeb2..3d84e0af2fb0e9e4cb62a7b25e4c1bd57a7420fa 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (** The "core" of an assertion is its maximal persistent part.
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index d9f02cf5bec7003bbec19138ab250dc564968cdc..676643d937cea5760e1bcc89be02a6ca5886821c 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -1,5 +1,6 @@
 From iris.base_logic Require Import base_logic soundness.
 From iris.proofmode Require Import tactics.
+Load iris_options.
 Set Default Proof Using "Type*".
 
 (** This proves that we need the ▷ in a "Saved Proposition" construction with
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 1e643d387856189f2324946663281821faac2997..b829a48ed2c62bc13a5d16f524b6eba576f7e868 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type".
+Load iris_options.
 Export invG.
 Import uPred.
 
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index 8029a018ad4f4e62432209e8dcf1d32d0c784e7a..e324f118095e88dc33093a48199929287f7fcead 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -2,7 +2,7 @@ From stdpp Require Import gmap gmultiset.
 From iris.base_logic Require Export derived.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import classes class_instances.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Class Fractional {M} (Φ : Qp → uPred M) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 74aa939fc3857aa58dda5dc21ef9425d47f9c84b..9f1814f84134d344d767c98c72f9f28a6018bf69 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import auth gmap frac agree.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 7ca2fc14458cef7cf150cb0a13f9d690c4119bd5..925e45a88790f0604a28c48c012779422d2b9903 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates namespaces.
 From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 95a378c30aa8827ddcf550230875418735cb816d..78874c60b8bf90731afa9c7b3a1c0178ce846230 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import iprod gmap.
 From iris.algebra Require cofe_solver.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** In this file we construct the type [iProp] of propositions of the Iris
 logic. This is done by solving the following recursive domain equation:
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 39fb911ddc3e9b91b85a84a5f7c6fa2c3fcfa311..cde5d9215b5efece58c6b00d6489ec9d0f3e9cbf 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (* Non-atomic ("thread-local") invariants. *)
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index a1b7774ce999e618848b1170fac892525de3ec52..3dc98fce0588fa077a9689327658f1d1e96aad0a 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -1,6 +1,6 @@
 From stdpp Require Export countable coPset.
 From iris.algebra Require Export base.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition namespace := list positive.
 Instance namespace_eq_dec : EqDecision namespace := _.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 24c20fae6444db93559828ad2ba7b0d5f997d6ce..ca5db516421d3876e2557b84eb45ab8c89d4ba9d 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import iprod gmap.
 From iris.base_logic Require Import big_op.
 From iris.base_logic Require Export iprop.
 From iris.proofmode Require Import classes.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 384e60c74b12ebcf86bc9cb9c6f32f39e451d2fa..bc5e2bbe29dc8ee9d0cc8d05f6174474faf8238b 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index ebfebfc343503af8c78625ac844b9f73c6b066d5..4f3e5a227e2f74b57973f695ac70001b539ab28a 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (** The CMRA we need. *)
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index b786ec65adac7ee76d8f14952878734f452b2c9f..312ca3ffa9e814660a0fa08f1f7f0925ab4f1c35 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P -∗ |={E1,E2}=> Q))%I.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index fe5e8da94ee7310e5ba34578ede8881ea35f50ad..a552f33be7e0849bd97043d5f30579b1f35c1fa2 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -3,7 +3,7 @@ From stdpp Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Module invG.
   Class invG (Σ : gFunctors) : Set := WsatG {
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index b471bfdaf41aed9c03752a96ecb401e42ee185cc..e26f98554866a7da2bf3c29cb9b8edb2a9d7fad5 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Export upred.
 From iris.algebra Require Export updates.
-Set Default Proof Using "Type".
+Load iris_options.
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index 105cb7503ed0ae3387c4ee7f8ae8148d5d02df01..491139c24a2a33c3a82de2c0632df4fe7bdf068d 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Section adequacy.
diff --git a/theories/base_logic/tactics.v b/theories/base_logic/tactics.v
index 0a75c4fb55477da496025bcbe936d97f0116f86d..5c3d7620a4e31c61f4149e45ec0374207f0de7e5 100644
--- a/theories/base_logic/tactics.v
+++ b/theories/base_logic/tactics.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap.
 From iris.base_logic Require Export base_logic big_op.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Module uPred_reflection. Section uPred_reflection.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 0ac232c72952ca916afb8f7c528a2d0d75b2bc15..23cb11b4619a4fb1c9a1dc6f5ea1451f5849317d 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** The basic definition of the uPred type, its metric and functor laws.
     You probably do not want to import this file. Instead, import
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 9a4a1115bb788463937d2e65bf991736fdc44549..db1c141fa3354e09226e44a976e4d9188191c72b 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 6c7a70a605dfe6d247f87767c6996d3c53ad0990..33fe54758505f39832ece8725bf89ce946fb1d20 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
 From stdpp Require Export strings.
 From stdpp Require Import gmap.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Module heap_lang.
 Open Scope Z_scope.
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index 93742d45b894592d09675a0f4c6b5d77485587bb..2a1cd1356817f613dbf69348c112d4c4311e2f2b 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition assert : val :=
   λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
diff --git a/theories/heap_lang/lib/barrier/barrier.v b/theories/heap_lang/lib/barrier/barrier.v
index 7ae83e5da15123f3fcb6dc59f83401ee1e923ac1..964276fde5535bac52d6ac8428002310073bc019 100644
--- a/theories/heap_lang/lib/barrier/barrier.v
+++ b/theories/heap_lang/lib/barrier/barrier.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export notation.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition newbarrier : val := λ: <>, ref #false.
 Definition signal : val := λ: "x", "x" <- #true.
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index 2bdce5c36927376aa33c3c4e64a3f29413175da7..4f5a38f0567918dad77a4c7a6145113e8d922f58 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -5,7 +5,7 @@ From stdpp Require Import functions.
 From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** The CMRAs/functors we need. *)
 Class barrierG Σ := BarrierG {
diff --git a/theories/heap_lang/lib/barrier/protocol.v b/theories/heap_lang/lib/barrier/protocol.v
index 1992abed4a66434436ca727d4a859107282d7df9..405edc6b3637339c0b451ebecb6ff0325d731fe3 100644
--- a/theories/heap_lang/lib/barrier/protocol.v
+++ b/theories/heap_lang/lib/barrier/protocol.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export sts.
 From iris.base_logic Require Import lib.own.
 From stdpp Require Export gmap.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** The STS describing the main barrier protocol. Every state has an index-set
     associated with it. These indices are actually [gname], because we use them
diff --git a/theories/heap_lang/lib/barrier/specification.v b/theories/heap_lang/lib/barrier/specification.v
index e3b16d18a76cabda5ea3393cf4b425bdfa578172..564ac3dd8504bc65ed034b99740efc5a627d69f5 100644
--- a/theories/heap_lang/lib/barrier/specification.v
+++ b/theories/heap_lang/lib/barrier/specification.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export hoare.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import proofmode.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Section spec.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 3e68d029742c336e2ba9c77ac026ef2a55050f66..881accd7d990c2fe17ddec2f2c10120429279b98 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac auth.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val := rec: "incr" "l" :=
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index f16c450e468d45fc1a527d940249e6863ad888ca..fba3534400535f6b780b24e17650bc494dbd3ce4 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Structure lock Σ `{!heapG Σ} := Lock {
   (* -- operations -- *)
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 6e289acc32306ea8615d16b29f33ab53b0898f76..d55f9f22d9001787cbe258da6484fb42d3695f40 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Definition parN : namespace := nroot .@ "par".
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 4c9b25a6a0de1e5135e84dab6a810015a8879371..a31e4b86cae232de8c07b36b02ebdff5e2701e2d 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition spawn : val :=
   λ: "f",
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 65375c186666ecc2b3813a828b6a634f2c7cfac0..8c6dc9bf75d807b370fdca2c0dfc44920add5abc 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 From iris.heap_lang.lib Require Import lock.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition newlock : val := λ: <>, ref #false.
 Definition try_acquire : val := λ: "l", CAS "l" #false #true.
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 3ec347a77a46337d23ed684b025f39da205fe60e..62fc6484a407fe1a27eb7479e309568ffa27029f 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth gset.
 From iris.heap_lang.lib Require Export lock.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Definition wait_loop: val :=
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index ec64faebe447f6932e25d912933ceefd9b36e4a9..522b32094b93eb7269b849b81fff7b81c3b4d1b7 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -5,7 +5,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (** Basic rules for language operations. *)
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index d2ee452b11bd94e8c93798cad18fde5eb0bd38c0..017edca77217668aa2fa226cf3540bff261813ca 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a793ec715a52a385be8c8dc8d6faf7566faa516e..8babb6d95192ede0e77d8a3409ac037fc430f315 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 1c040a9472665570c95a71ed86f0c904d8ba720c..fb2b73a38d1d811aefe854c8ae25188f5ccab6a8 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export lang.
-Set Default Proof Using "Type".
+Load iris_options.
 Import heap_lang.
 
 (** We define an alternative representation of expressions in which the
diff --git a/theories/iris_options.v b/theories/iris_options.v
new file mode 100644
index 0000000000000000000000000000000000000000..451f266bc56d6745a0caf63e779f1a8681b130e0
--- /dev/null
+++ b/theories/iris_options.v
@@ -0,0 +1 @@
+Set Default Proof Using "Type".
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 2c9ce1d1eb1a2817bd0181cb402b3d5cbef7cb27..6e65c18518f76afe768e0fad7ae72c590d6e598b 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 (* Global functor setup *)
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 646ebbdcae4658fce73c6687eeeab2ec76b10241..96c00686dc37d21157b7f40948dcd5e2c4b3ffd0 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -2,7 +2,7 @@
     that this gives rise to a "language" in the Iris sense. *)
 From iris.algebra Require Export base.
 From iris.program_logic Require Import language.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index e0c0f468b7a493ae7de2a48c196d64249de57361..dc4a4b7fd19da24578b665e28fd834d4c8b0ce4b 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,7 +1,7 @@
 (** 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".
+Load iris_options.
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index ee98518676af7ea9a0793f00f21d1244f8c43bab..0bcfa16e0746ea18e4f1936e9afb85487a43a3a8 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -2,7 +2,7 @@
     a proof that these are instances of general ectx-based languages. *)
 From iris.algebra Require Export base.
 From iris.program_logic Require Import language ectx_language.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index bb4489e5eca99d6bb84ff329c5078b7e08cd34c6..047d99b093cc9c6f7e0bb986bdccb0d7c28f625f 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 21fc2e3a1428bd494a955b691a4ad77426a111c1..c543666ea0e4b4b4cf662814dd782ad641df11b3 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Structure language := Language {
   expr : Type;
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 1e69da79f511637821139b170aae535ca2fcd8ac..d6ed7863505638fc6a48aee0dbb68cac8c3d2412 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic Require Export big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Section lifting.
 Context `{irisG Λ Σ}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 6d318ea72a2476bcea8a88cdfe74a01d090549d5..17bdee8f663ca867b58684be8adef2c77d73c6a8 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
 From iris.algebra Require Import auth.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 70acaa8dc93d95458b595c5c42379d1ab8c73d00..3d029a4a07b4048482796d2c5ebb86dde3c516b5 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 3e985fc46c3c3ebde5a9993b0e70cb6fab5cce10..fdeaa26bfec86f1dbbbc6f0cd6941acfa8f94887 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Export classes.
 From iris.algebra Require Import gmap.
 From stdpp Require Import gmultiset.
 From iris.base_logic Require Import big_op.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Section classes.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 6efe527662568ab32db07f3a09362f5e87ca17ee..ff0a1e88dc4984f5153e65df896fed8a257dda8d 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 
 Class FromAssumption {M} (p : bool) (P Q : uPred M) :=
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 7137e4ec08b65311ee9083bea9187c1c1b7deb1e..7e817fee7bf3b1a6f2f22b0542e2b79c23d0d421 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -2,7 +2,7 @@ From iris.base_logic Require Export base_logic.
 From iris.base_logic Require Import big_op tactics.
 From iris.proofmode Require Export environments classes.
 From stdpp Require Import stringmap hlist.
-Set Default Proof Using "Type".
+Load iris_options.
 Import uPred.
 Import env_notations.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 8ed1a9bf68c27eff6218e374fdc5d9392c461a8a..f1f3bf496fca534e245a8f8019b3a7ab68e41685 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -2,7 +2,7 @@ From stdpp Require Export strings.
 From iris.proofmode Require Import strings.
 From iris.algebra Require Export base.
 From stdpp Require Import stringmap.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Inductive env (A : Type) : Type :=
   | Enil : env A
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index c1cc121e820ccdfd68ad3b571b9a32d36d9982eb..f58aa266f9dcf69715fefe34ebd68f8622c4d5c4 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,5 +1,5 @@
 From stdpp Require Export strings.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Inductive intro_pat :=
   | IName : string → intro_pat
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index ab6893379e1966040d2e98758527bf3f124dfd86..3f112f2e7ad5f3a99e5fe66ed0aa3966abfde56f 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics environments.
 From stdpp Require Export strings.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Delimit Scope proof_scope with env.
 Arguments Envs _ _%proof_scope _%proof_scope.
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index b019b2c53c5cbefaca75b16255500894c7758cba..bef4398ca45ed7e1de1b593f30280379e7aea8c6 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -1,5 +1,5 @@
 From stdpp Require Export strings.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Inductive sel_pat :=
   | SelPure
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index a33322ee4f02cdb52c054810959a026d71f469aa..3860abb6dc463f0f5ed0a0d4796f7c8cdb095b7f 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,5 +1,5 @@
 From stdpp Require Export strings.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Record spec_goal := SpecGoal {
   spec_goal_modal : bool;
diff --git a/theories/proofmode/strings.v b/theories/proofmode/strings.v
index bde47e5bfc932adce078ccbc0c4bbaf03cde8b4e..73f8e04398e8c5689f70c74e0fa60d2e67fb17bc 100644
--- a/theories/proofmode/strings.v
+++ b/theories/proofmode/strings.v
@@ -1,7 +1,7 @@
 From stdpp Require Import strings.
 From iris.algebra Require Import base.
 From Coq Require Import Ascii.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 0d99ef960f2a98643342024006ffebe8a81df446..1dc07617306f6008d68b45558fb7617334e07a84 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From stdpp Require Import stringmap hlist.
 From iris.proofmode Require Import strings.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Declare Reduction env_cbv := cbv [
   beq ascii_beq string_beq
diff --git a/theories/tests/barrier_client.v b/theories/tests/barrier_client.v
index 4c5992d36db3c70854751f8a0e4cbd3e9ded87a3..5fed1bf2d6f12a5d419e5865ed745b7077e46752 100644
--- a/theories/tests/barrier_client.v
+++ b/theories/tests/barrier_client.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.heap_lang Require Import adequacy proofmode.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition worker (n : Z) : val :=
   λ: "b" "y", wait "b" ;; !"y" #n.
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 478e09a0c0df1cdafd863a10bae87fcdf23ea640..a26a12a6454f30298c3cca7278ee7d4841de4e7d 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Section LiftingTests.
   Context `{heapG Σ}.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 3449ede5e4c5e830579a0d98920123a0ac7f3acf..b1a66b0822664dbebd0f516578c4cd7a1540f56d 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -2,7 +2,7 @@ From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export hoare.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+Load iris_options.
 
 (** The proofs from Section 3.1 *)
 Section demo.
diff --git a/theories/tests/joining_existentials.v b/theories/tests/joining_existentials.v
index e0505abc7deb53c46e25c7e0a6a7abaaa3d606e3..67b19c1ca07d327bd94a8b35d6e32095e873ab74 100644
--- a/theories/tests/joining_existentials.v
+++ b/theories/tests/joining_existentials.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import excl agree csum.
 From iris.heap_lang.lib.barrier Require Import proof specification.
 From iris.heap_lang Require Import notation par proofmode.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
   csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
diff --git a/theories/tests/list_reverse.v b/theories/tests/list_reverse.v
index cdee426298fe1fe1c6071af8ae295eec01d4f21d..0df205e57f5291f00d8b368db62a73ef3bc638ed 100644
--- a/theories/tests/list_reverse.v
+++ b/theories/tests/list_reverse.v
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Section list_reverse.
 Context `{!heapG Σ}.
diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index fd8c836b2c629f1c009068484be2113f11176c1f..74accb318ab491d9694d3f591dfe89488cdf4504 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
 From iris.heap_lang Require Import assert proofmode notation.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 28e5da973fabe6091e337a04d4edacb6beae5eb7..9b423dfa6986e2fd7820cacb49852fb1d01cfaf7 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
   □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index dfcb13d2dc5c18cf9110ea16a3e4e917ce869bfd..359a5425a3daa53b7381bace03dcd9b35d074b39 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+Load iris_options.
 
 Inductive tree :=
   | leaf : Z → tree