diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 3320476460e984564768221c7f9da4816a1f28a8..d2783d6eca4722c168f1359e10a21f4cde26af25 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.
+From iris Require Import options.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
@@ -50,7 +51,6 @@ Proof.
 Qed.
 
 Section agree.
-Local Set Default Proof Using "Type".
 Context {A : ofeT}.
 Implicit Types a b : A.
 Implicit Types x y : agree A.
@@ -276,7 +276,7 @@ Section agree_map.
   Context {A B : ofeT} (f : A → B) {Hf: NonExpansive f}.
 
   Instance agree_map_ne : NonExpansive (agree_map f).
-  Proof.
+  Proof using Type*.
     intros n x y [H H']; split=> b /=; setoid_rewrite elem_of_list_fmap.
     - intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver.
     - intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 8ae2868442822f026dfb6fffe0a705a9a6afb215..8c6a51f9fef68d37fc5b7c0266825f9e06f0484c 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Export frac agree local_updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types
   of elements: the fractional authoritative `●{q} a`, the full authoritative
diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 603e9c20cebe850070a8c639514fcc2949b87a97..3341e502cf497ec86ed06e360a618273c1a500c5 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,6 +1,6 @@
 From Coq.ssr Require Export ssreflect.
 From stdpp Require Export prelude.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Global Open Scope general_if_scope.
 Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
 Ltac done := stdpp.tactics.done.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b56fade14a8b34408d61adcc1aca5ca15e336e53..a3d20798d9166cf2d72f88f76d68191431cb2aa7 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,6 +1,6 @@
 From stdpp Require Import finite.
 From iris.algebra Require Export ofe monoid.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Class PCore (A : Type) := pcore : A → option A.
 Hint Mode PCore ! : typeclass_instances.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 0cae57b57d96f71b44334bfa34b3e2e92379b403..2cff617b22b1e5c94cde5e377f3e7753a4a38d7f 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -1,7 +1,7 @@
 From stdpp Require Export sets coPset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type".
+From iris Require Import 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 f5a1900511bf1f0f1070cd9fa319f9ef1e9064a9..3fd8fe1689a83ee2bdbc49a5b4fbb055cdb5a92c 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".
+From iris Require Import options.
 
 Record solution (F : oFunctor) := Solution {
   solution_car :> ofeT;
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index e6b483a424a9a60b5e7b4000b731f8d241ff77ee..5931a885044c505d203c2bd1c82126cf5db67f8b 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import local_updates.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index 9b58faaa19e075ad2a181530563ec844059d5c15..1e890200156681335fcd750d46196c99cec27e1f 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".
+From iris Require Import options.
 
 Record DraMixin A `{Equiv A, PCore A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index a61d5e214c3089430562acb09e1e5d0a3d05f852..fcf4f879d34ff9736684b0eaddc5b652f44ed1b8 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".
+From iris Require Import options.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 737208fd782cbdde15c2bb482b3692257e1613cf..121c54296ffb66dbda311719239df92be000eba3 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -6,7 +6,7 @@ validity of the unbounded fractional camera [ufrac]. *)
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import proofmode_classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Since the standard (0,1] fractional camera is used more often, we define
 [frac] through a [Notation] instead of a [Definition]. That way, Coq infers the
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index 893c56e0b2915fa738db34af7c6d417062fbdbb6..1d7353182eea738249eefc391e8a52eebd9bfb69 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -1,7 +1,7 @@
 From stdpp Require Import finite.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT}
     (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 6e3b7311afb29d4aa687e015c12eee757be176f4..714a62663e71eb8ec800f54b6e9c593f767ff851 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -2,7 +2,7 @@ From stdpp Require Export list gmap.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates proofmode_classes.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section cofe.
 Context `{Countable K} {A : ofeT}.
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 6951db04bad8fe3aa9def5cbac822105fac039e6..701bb9d5a942f4988efadbe285640dc88c138d3a 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -1,7 +1,7 @@
 From stdpp Require Export sets gmultiset countable.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (* The multiset union CMRA *)
 Section gmultiset.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index eb7751229d832969f04eb407b681590492314571..b3a5d578c42c8fef3286ea5bde298c442df02394 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,7 +1,7 @@
 From stdpp Require Export sets gmap mapset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (* The union CMRA *)
 Section gset.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 50ceac0f10662f859749bf436c378496fb01ec93..5c94e79b684c3113c3b5163a60ba3bfef0a11c3b 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -2,7 +2,7 @@ From stdpp Require Export list.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section cofe.
 Context {A : ofeT}.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 199a7c16dc71c37ee8f8b018a411fa17a722507f..7a02bd42db701a5bcea62b77de7ec4b05cab814e 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".
+From iris Require Import options.
 
 (** * Local updates *)
 Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
diff --git a/theories/algebra/monoid.v b/theories/algebra/monoid.v
index 57e6a5efd54dfe26518127b8a8c50ff8794b8819..239d2d7fee0d65f68f5f5e5b61cc7a6a23643eef 100644
--- a/theories/algebra/monoid.v
+++ b/theories/algebra/monoid.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** The Monoid class that is used for generic big operators in the file
 [algebra/big_op]. The operation is an argument because we want to have multiple
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index aaf7e2a71d27226dbd5efc96962582f86c431dca..7474b7e2c9c993969b46ae71e4ad353c13cc7112 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -1,7 +1,7 @@
 From stdpp Require Import namespaces.
 From iris.algebra Require Export gmap coPset local_updates.
 From iris.algebra Require Import updates proofmode_classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** The camera [namespace_map A] over a camera [A] provides the connectives
 [namespace_map_data N a], which associates data [a : A] with a namespace [N],
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c54e539c377bb13a6656fdf7e242e11a3e3e25f5..663f28440d427346f5b3882baf46fcdf8c94bbc7 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".
+From iris Require Import options.
 Set Primitive Projections.
 
 (** This files defines (a shallow embedding of) the category of OFEs:
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 5b4c19f5f6aef09c317b2078d824836cf7ded31a..29682927c857afd3ee4f7c6a12fb1b6cba246666 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,7 +1,7 @@
 From stdpp Require Export propset.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index 42d9645d7bf3d47fee58e245c3692957ba9c3797..ed629c467bcc4a01cd13837ddc263a50431910d8 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -3,7 +3,7 @@ elements are in the interval (0,..) instead of (0,1]. *)
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import proofmode_classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Since the standard (0,1] fractional camera [frac] is used more often, we
 define [ufrac] through a [Definition] instead of a [Notation]. That way, Coq
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 00462f7cbe04dbb4e4bcee91bc4deee530acaf92..b8328574873f5ec73df22103bd93aeac3c55e8c7 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".
+From iris Require Import 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 a72c887bb918d58b4026a3a1b63ea0355ec660bf..dd904042e1b9c7bd2911d6c18e36b129f8c087fa 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".
+From iris Require Import options.
 
 Section ofe.
   Context {A : ofeT}.
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 13c4da99453751133025fb27e4f4fbaab2916bb2..d6fea5a090b9708672ca42148eaa11c0a2581e8d 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export bi.
 From iris.base_logic Require Export derived proofmode.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (* The trick of having multiple [uPred] modules, which are all exported in
 another [uPred] module is by Jason Gross and described in:
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 01dff355c205c86e21914865c8f0bc720b3442af..b3f0cee87069a59a0f5b64e50a8e2832f1854a85 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export bi.
 From iris.base_logic Require Export bi.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.bi base_logic.bi.uPred.
 
 (** Derived laws for Iris-specific primitive connectives (own, valid).
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index d5d4ade215f6820fe2aa64c257645ade9c74f07f..a642742e64e396ff079253bb4903da856f722d08 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index eaea54618da18fe222d60306223fb25488d6747d..a02be5297f8151f7e2c7ff47ed4eac299b4ce21b 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import lib.excl_auth gmap agree.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
+From iris Require Import 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 234123b5737f249edd5ed8f37b9881a652932c19..ab3325748ebf2f5f0b26db573e1bc048186dc2eb 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -2,7 +2,7 @@ From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Export frac.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index a9867444208f8cdf3ea4028556aa3b01e5141183..ccd4ac39cf70d7b97817fe6de67f40db9fb42ac0 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import wsat.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Export invG.
 Import uPred.
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index efe8eb9b2059770cfc69852d98f83ec8cbbb5756..3d57ed0509f4d992f3bd5b1da19f961cc0a8ffe7 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -3,7 +3,7 @@ From iris.bi.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap frac agree namespace_map.
 From iris.base_logic.lib Require Export own.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (** This file provides a generic mechanism for a point-to connective [l ↦{q} v]
diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index 230ce99431a926d5e84ff2d78df2d298696b4c58..b371e4b0696474ef95eb87c1f35c944cc2d80616 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Import auth excl gmap.
 From iris.base_logic.lib Require Import own invariants gen_heap.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** An "invariant" location is a location that has some invariant about its
 value attached to it, and that can never be deallocated explicitly by the
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 4ddbe68958da21bc8cc39ce7f8fdd54b731cfcb6..adff4f6eb0a06733e346c854757bbc8bc6f9323a 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.base_logic.lib Require Import wsat.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (** Semantic Invariants *)
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 214b72850c101e4e1f8aaf83831e9f9d114be7e3..a40c6d1cf1072d3c87d58abfc50b89fc9e9a3bd3 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Import gmap.
 From iris.algebra Require cofe_solver.
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
+From iris Require Import 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 00d4452b89f0ce61aeb6ba950d4555544d19b1e9..c991982418c605ceca2c0ca42c45c324447fdf58 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gset coPset.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (* Non-atomic ("thread-local") invariants. *)
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index ed77ef6f19e44e81add28bea10c5f2a00aff89a2..15157285986ae634f6e016d7ba7fca72455ddcf1 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import functions gmap proofmode_classes.
 From iris.base_logic.lib Require Export iprop.
-Set Default Proof Using "Type".
+From iris Require Import 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/proph_map.v b/theories/base_logic/lib/proph_map.v
index 6793cd7a74904761aeb3c9097029d59f1abd468f..25391b5c9d55c5a567004f003838cac7eba33def 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth excl list gmap.
 From iris.base_logic.lib Require Export own.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 Local Notation proph_map P V := (gmap P (list V)).
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index ea836c5104303296b18683deee4c58b6a0a25e24..6480491143fe253f52c76cc47e36087ead06745a 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -2,7 +2,7 @@ From stdpp Require Import gmap.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import agree.
 From iris.base_logic Require Export own.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (* "Saved anything" -- this can give you saved propositions, saved predicates,
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 05abc0e46770dae5df506d1cfd8b6d5dab3bbec2..30ceaa1108423c9b6fec4c7edfb2a3c76707cd7a 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Export sts.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (** The CMRA we need. *)
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index d94376bc77d5d956fc080c3089f0598ab4fcae7c..04b3358364c02d6eeb98d2ecefb8c9c50c47944a 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   □ (P -∗ |={E1,E2}=> Q).
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 1846c891253252d811f061f96c6afbed51a5bf27..b665b0562efd6e3b109f7f96dbb3d0890e353b25 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -2,7 +2,7 @@ From stdpp Require Export coPset.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic.lib Require Export own.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** All definitions in this file are internal to [fancy_updates] with the
 exception of what's in the [invG] module. The module [invG] is thus exported in
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index fe44e03230e8ab0cde1d8fd13a986b0e558ae034..569746e0a40a02e004b40738dce44e0653bd4e1b 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,7 +1,7 @@
 From stdpp Require Import finite.
 From iris.bi Require Import notation.
 From iris.algebra Require Export cmra updates.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|] : core.
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption] : core.
 Local Hint Extern 10 (_ ≤ _) => lia : core.
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 8f5aa1aa0fc72846c4cc3cd612ef2e95d2756b1e..66afc4ad7ea0f1b1e48c0fce76b75777b27a528e 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export derived_laws derived_laws_later big_op.
 From iris.bi Require Export updates internal_eq plainly embedding.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Module Import bi.
   Export bi.interface.bi.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 768a357574099eea137bb9fb49594412fe1e93fa..1d0fd6e21ef8b2f8c331d1858de172afdf7e7ab7 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1,7 +1,7 @@
 From stdpp Require Import countable fin_sets functions.
 From iris.bi Require Import derived_laws_later.
 From iris.algebra Require Export big_op.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** Notations for unary variants *)
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index bea7c66396f0ac47a3191c5da84fc066bc647771..d79d71a8508ad103c001ce7bf95f59c31164a694 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -2,7 +2,7 @@ From stdpp Require Import coPset namespaces.
 From iris.bi Require Export bi updates laterable.
 From iris.bi.lib Require Import fixpoint.
 From iris.proofmode Require Import coq_tactics tactics reduction.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Conveniently split a conjunction on both assumption and conclusion. *)
 Local Tactic Notation "iSplitWith" constr(H) :=
diff --git a/theories/bi/lib/core.v b/theories/bi/lib/core.v
index aa4001d33c7248f16cfb78bec0d004d7681c3418..dc67214dc5e3844f94a5a6f8bcf082545f733d4b 100644
--- a/theories/bi/lib/core.v
+++ b/theories/bi/lib/core.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export bi plainly.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 (** The "core" of an assertion is its maximal persistent part,
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 51253b19f4c192a4da0bb62e86b1ea5c1f38f937..1721e6840cd86608ffcb3383a584d23bbe78040d 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -1,6 +1,6 @@
 From iris.bi Require Export bi.
 From iris.proofmode Require Import classes class_instances.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 7983c6fb6631164b9a3ba4db261a216b68d7408d..eaac68789a4775ffa7c5695d86019370bd8d3915 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.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.
 
 (** The class of laterable assertions *)
 Class Laterable {PROP : bi} (P : PROP) := laterable :
diff --git a/theories/bi/tactics.v b/theories/bi/tactics.v
index feb33d0fb9540cd9737bbe8a9db4253cf81db45c..8881d03dcb93d28d8bef7b71fc40b5df6b82e8ef 100644
--- a/theories/bi/tactics.v
+++ b/theories/bi/tactics.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap.
 From iris.bi Require Export bi.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Module bi_reflection. Section bi_reflection.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index bce15e435908cceec9018bb8ff1fb6cf07ee72d5..56616ba1a34cb0e3a4e3b167dc882e3a81bef077 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
diff --git a/theories/heap_lang/derived_laws.v b/theories/heap_lang/derived_laws.v
index c2aafac5b642f6d5e748a93c6694988b830f0667..4a394f6b61070c69a0f76ba688108bce23634226 100644
--- a/theories/heap_lang/derived_laws.v
+++ b/theories/heap_lang/derived_laws.v
@@ -9,7 +9,7 @@ From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export primitive_laws.
 From iris.heap_lang Require Import tactics notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** The [array] connective is a version of [mapsto] that works
 with lists of values. *)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 52616a5aa8c706e47839f5511f054c7296b00dfb..d23eabdd276e433845aad08bc09b5804c86c090e 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -3,7 +3,7 @@ From stdpp Require Import gmap.
 From iris.algebra Require Export ofe.
 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.heap_lang Require Export locations.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** heap_lang.  A fairly simple language used for common Iris examples.
 
diff --git a/theories/heap_lang/lib/arith.v b/theories/heap_lang/lib/arith.v
index bbaf8716d60ae9b68466d0a3fab641f32a191623..501cfbabc553961293159f97b3f09c584ac61d68 100644
--- a/theories/heap_lang/lib/arith.v
+++ b/theories/heap_lang/lib/arith.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** A library defining binary [minimum] and [maximum] functions, together with
 their expected specs. These operations come up often when working manipulating
diff --git a/theories/heap_lang/lib/array.v b/theories/heap_lang/lib/array.v
index b41447205a3e874946ea48a82926baa566666eb0..8a16448b85f7deb1f611161d4487aa9873f629c5 100644
--- a/theories/heap_lang/lib/array.v
+++ b/theories/heap_lang/lib/array.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Provides some array utilities:
 
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index b8c932ef13879b50dfcca1eb5a44895194718dc4..db8adb8d66004abb466db5c50c685babc34c13e3 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition assert : val :=
   λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index bdbc3783861f96a61fd7f797d258353b2b81ecaf..f39fc9d07de43e278ffecb761c0b28b8955b321d 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import notation proofmode.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** A general logically atomic interface for a heap. *)
 Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 2e41a59055412d4e527dc2a5d51cc328ebed7681..0cc86cfab7a83652c4f13494edb531a0014a8559 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val := rec: "incr" "l" :=
diff --git a/theories/heap_lang/lib/diverge.v b/theories/heap_lang/lib/diverge.v
index 1a34a029cba12015850f093b1db27a2b237e49a6..393445f46dc820636a3aaaa8d761e18de35dcdca 100644
--- a/theories/heap_lang/lib/diverge.v
+++ b/theories/heap_lang/lib/diverge.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** This library provides a [diverge] function that goes into an infinite loop
 when provided with an (arbitrary) argument value. This function can be used to
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index b479bc96ad7cfc72515c00a93748d766b2ed7a1e..bf71e6f3b72336af0834728ee6c88ae3ac2d966a 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap par.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Show that implementing fetch-and-add on top of CAS preserves logical
 atomicity. *)
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 0430aec748b016e6935baee9c52802fa5b03b639..8edd581e41b0f4ea071e6b026be64b4c116c3ee4 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import primitive_laws notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Structure lock Σ `{!heapG Σ} := Lock {
   (** * Operations *)
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index a9378e5992195b885a57c06ea5706f16e36e5fbc..fb33eb8003808a792c6c09a7974c16d040bc9a69 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang Require Export spawn.
-Set Default Proof Using "Type".
+From iris Require Import 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 78bb229190d7606b06c4f38ce1033e09768976af..9b10f92472869c843437e1be3b9f97258c6f5f32 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition spawn : val :=
   λ: "f",
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 33d4fa87f7dc2458b2cb69172ba26509b3422583..1e5af4e7310de9c20b5c0c587799196ec5d57bd6 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import lock.
-Set Default Proof Using "Type".
+From iris Require Import 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 311c7ae2146c0350cd18c3591860aa65a90d7424..0947e7b54156fa88b365e437159d3a3ec5bb8d09 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Export lock.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 Definition wait_loop: val :=
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 6e60bbd0a8928ab6301a18cfd530f0c48493b297..f9948af37616d34af23209e3c10426d537324c3b 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.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** Coercions to make programs easier to type. *)
 Coercion LitInt : Z >-> base_lit.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index ecc290cff8b287d7b8bc521513b8a04af9d40140..5edc89f8f15619b95ab843fa4641ca3b59d58acc 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -10,7 +10,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index f3280b9fc205b53e511b3e8d29ec9cec3c720eb4..d24214eb7d8e8d249014237e7ee17df51914de6c 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Export tactics.
 From iris.program_logic Require Import atomic.
 From iris.heap_lang Require Export tactics derived_laws.
 From iris.heap_lang Require Import notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 Lemma tac_wp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index c3325b8dd09014e4bd41247f0d138379b93c37b7..9b19bb9a638b24c9eef139c409bb07887535284e 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".
+From iris Require Import options.
 Import heap_lang.
 
 (** The tactic [reshape_expr e tac] decomposes the expression [e] into an
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 8aa59f739f02b93d25b6a25c87847cb1aa6b39ee..abb6118c752c1feb3c1451671ae15a6fd3aa3d64 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export total_adequacy.
 From iris.heap_lang Require Export adequacy.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
   (∀ `{!heapG Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]) →
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index a2bcf4e653069722ec8fde488cac54c47b51653c..599c09a10b3d6cefe503d03c7c7fe70da8db9702 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic.lib Require Import wsat.
 From iris.program_logic Require Export weakestpre.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (** This file contains the adequacy statements of the Iris program logic. First
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index c035e92bcc333b1d295ff0eed667812fb61d722a..13be0ce35f1feccebdedc00a519b03f293f3dfa1 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -4,7 +4,7 @@ From iris.bi.lib Require Export atomic.
 From iris.proofmode Require Import tactics classes.
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic Require Import invariants.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (* This hard-codes the inner mask to be empty, because we have yet to find an
 example where we want it to be anything else. *)
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 1894ba20ecd6113b74f71840766e37ebabdbcefa..774fe60df50e62610d1da6700c25106f6b45ad27 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".
+From iris Require Import options.
 
 (** TAKE CARE: When you define an [ectxLanguage] canonical structure for your
 language, you need to also define a corresponding [language] canonical
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 7af252db44c1a8f7981a50943806cacffe078241..926ae75c554eb27f2e558bde25d825ee3bf28608 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.proofmode Require Import tactics.
 From iris.program_logic Require Export ectx_language weakestpre lifting.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section wp.
 Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index d647c618a2776876ee3d5e031336a1a137d85655..e9e9477c5f5a7a61ff9b1b534c87a3b936fa9058 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".
+From iris Require Import options.
 
 (** TAKE CARE: When you define an [ectxiLanguage] canonical structure for your
 language, you need to also define a corresponding [language] and [ectxLanguage]
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 6eb2e36dca41edc24c4e8849da692d1a1019067d..b08d144fbf58be19cb1f5b1fc59932d77ba06fe3 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export viewshifts.
 From iris.program_logic Require Export weakestpre.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 6999e0163729febb50529156bf16a54670774044..fb982fd7cd6ad03be42222bdc14375fc6e1a202c 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".
+From iris Require Import options.
 
 Section language_mixin.
   Context {expr val state observation : Type}.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 9a2d292e46e942b78e59f8a3bf3c57a5007bb9ea..bb5fa43d662c2d450ab3c0edfbef4498ff35574e 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -3,7 +3,7 @@ semantics to the program logic. *)
 
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section lifting.
 Context `{!irisG Λ Σ}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 7098222ab80bd4aadcb74aa782204dd154a9ef9f..0b5b33fc70b8d72ae5f1b0b99e4accb5a10a88c2 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import lib.excl_auth.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (**
 This module provides an interface to handling ownership of the global state that
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 774dbf1d7ed7c8b96c1197f3d2d929af98391fa2..731f690798d8411b479846f275fea521d7dfd027 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -2,7 +2,7 @@ From iris.bi Require Import big_op fixpoint.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.program_logic Require Export total_weakestpre adequacy.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 Section adequacy.
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index 9fe8e494e0933034cf83b705b770773f2579d324..99c34b6d3b85db35fff72f208b3aa6046af791f2 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -1,7 +1,7 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export ectx_language total_weakestpre total_lifting.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section wp.
 Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index eaf71db025ebc7016290dc2fa54b8fe52880ea10..19b9af5a28a72f19f3234397d44ab6adf2b952c4 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -1,7 +1,7 @@
 From iris.bi Require Export big_op.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export total_weakestpre.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Section lifting.
 Context `{!irisG Λ Σ}.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 51604339186b0091c63e4276d418ec9fee047d3f..06f722a4fdcf9a211ef9f299c8677c6a609e2b6b 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -1,7 +1,7 @@
 From iris.bi Require Import fixpoint big_op.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 (** The definition of total weakest preconditions is very similar to the
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 8c2cb8f9a26722508ea118e00d474a865a082306..e0d639fb6695e7c444be1b52e18ac02f97c323b8 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export language.
 (* FIXME: If we import iris.bi.weakestpre earlier texan triples do not
    get pretty-printed correctly. *)
 From iris.bi Require Export weakestpre.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import uPred.
 
 Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index e50c8c88d01afe04a894150f55358621b3b51f45..abf4e1361f3018b81cf72a25d2a288f61c5a1a23 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -1,7 +1,7 @@
 From Coq Require Export Ascii.
 From stdpp Require Export strings.
 From iris.algebra Require Export base.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 (** * Utility definitions used by the proofmode *)
 
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 17ec680c25e50227aa9f1962b551370850f843e0..2ee7a4d62d986402a54cb9d7f2c4911cfb90ca3b 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -2,7 +2,7 @@ From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi telescopes.
 From iris.proofmode Require Import base modality_instances classes.
 From iris.proofmode Require Import ltac_tactics.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 (* FIXME(Coq #6294): needs new unification *)
diff --git a/theories/proofmode/class_instances_embedding.v b/theories/proofmode/class_instances_embedding.v
index c7fd3a108280af274f49f1728a8585162b1bbcd6..c75f275345fa173a6eadf31178ac849ec2179c89 100644
--- a/theories/proofmode/class_instances_embedding.v
+++ b/theories/proofmode/class_instances_embedding.v
@@ -1,6 +1,6 @@
 From iris.bi Require Import bi.
 From iris.proofmode Require Import modality_instances classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 (** We add a useless hypothesis [BiEmbed PROP PROP'] in order to make sure this
diff --git a/theories/proofmode/class_instances_internal_eq.v b/theories/proofmode/class_instances_internal_eq.v
index c33c76c7929de18128c85c4b968a358ad75208d0..c75ead317fd516cc433597c003cc86ee774ba5e4 100644
--- a/theories/proofmode/class_instances_internal_eq.v
+++ b/theories/proofmode/class_instances_internal_eq.v
@@ -1,7 +1,7 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi.
 From iris.proofmode Require Import modality_instances classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Section class_instances_internal_eq.
diff --git a/theories/proofmode/class_instances_later.v b/theories/proofmode/class_instances_later.v
index bae07582ca9011b469aae77a3571d999060b18fc..1f850ff695d125d8c235ac5bf4c5e0fba3486e56 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/theories/proofmode/class_instances_later.v
@@ -1,7 +1,7 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi.
 From iris.proofmode Require Import modality_instances classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Section class_instances_later.
diff --git a/theories/proofmode/class_instances_plainly.v b/theories/proofmode/class_instances_plainly.v
index d7b20bb9e5c60a19f6e9bab3501d09b693461f99..f3eba370e60e2c96f850a1b3bda79af5454bc51f 100644
--- a/theories/proofmode/class_instances_plainly.v
+++ b/theories/proofmode/class_instances_plainly.v
@@ -1,6 +1,6 @@
 From iris.bi Require Import bi.
 From iris.proofmode Require Import modality_instances classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Section class_instances_plainly.
diff --git a/theories/proofmode/class_instances_updates.v b/theories/proofmode/class_instances_updates.v
index 8a3f52152e16ed418180489ef8a34c9a30c106e3..9bc9f38aa36b7772b16d121c721bbe02e328a089 100644
--- a/theories/proofmode/class_instances_updates.v
+++ b/theories/proofmode/class_instances_updates.v
@@ -2,7 +2,7 @@ From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi.
 From iris.proofmode Require Import modality_instances classes.
 From iris.proofmode Require Import ltac_tactics class_instances.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Section class_instances_updates.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 307c4034986f725beb0b8a888b03fc182e3d981f..50f03e157d61c5917833141a49e896d075175ebf 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -2,7 +2,7 @@ From stdpp Require Import namespaces.
 From iris.bi Require Export bi.
 From iris.proofmode Require Import base.
 From iris.proofmode Require Export ident_name modalities.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 871159211440d3c94eda784b68807f4fb841e84d..72a33aa275affe6926e032d71a74765ea04508c7 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1,7 +1,7 @@
 From iris.bi Require Export bi telescopes.
 From iris.bi Require Import tactics.
 From iris.proofmode Require Export base environments classes modality_instances.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 Import env_notations.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index d9eea54a46d00bb9b3e61d34eff3060c5cfe4d53..84713ce14177f0dfec2039be135af958ef5a0cac 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -2,7 +2,7 @@ From iris.bi Require Export bi.
 From iris.bi Require Import tactics.
 From iris.proofmode Require Import base.
 From iris.algebra Require Export base.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Inductive env (A : Type) : Type :=
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 3e909d0b158d53072819476ed7a37174a0776713..5a86fc7ca5ae6d13b16f155478e308f345b06fda 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -1,7 +1,7 @@
 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics telescopes.
 From iris.proofmode Require Import classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 (** This file defines the instances that make up the framing machinery. *)
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 1d3cb9922fbcf41d9f08a6227a81ac6ed649e46b..d5895ebdcfa6c267dbb18d9dadf0b436aab46bad 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,6 +1,6 @@
 From stdpp Require Export strings.
 From iris.proofmode Require Import base tokens sel_patterns.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Inductive gallina_ident :=
   | IGallinaNamed : string → gallina_ident
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 203f53c92d97d63f7900982c39036b169aa9d54c..92d12aacdbde1e8ea812dbb43e6b685152968b61 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -3,7 +3,7 @@ From iris.bi Require Export bi telescopes.
 From iris.proofmode Require Import base intro_patterns spec_patterns
                                    sel_patterns coq_tactics reduction.
 From iris.proofmode Require Export classes notation.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Export ident.
 
 (** For most of the tactics, we want to have tight control over the order and
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index b4a5e0236ef6cc4d0001073bdaa3fa90f6b92418..cc33f63bd1c3a5f3712a78d5142400c20f2da66c 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -1,6 +1,6 @@
 From stdpp Require Import namespaces.
 From iris.bi Require Export bi.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 (** The `iModIntro` tactic is not tied the Iris modalities, but can be
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index f586244c6c9695aad44800aa7be34b669cc3408a..23d93c65e33cbbd392e48304fafa74359270e381 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -1,6 +1,6 @@
 From iris.bi Require Import bi.
 From iris.proofmode Require Export classes.
-Set Default Proof Using "Type".
+From iris Require Import options.
 Import bi.
 
 Section modalities.
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 0025dc12ea87204306b49c36d7e45303a6204741..d2812ef7a44f24bf2ded5eb1a0ab87bce1c48fef 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -1,6 +1,6 @@
 From stdpp Require Export strings.
 From iris.proofmode Require Import coq_tactics environments.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Declare Scope proof_scope.
 Delimit Scope proof_scope with env.
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index aac295086d279447dbe4fea413a514496a81676a..0b360c19647ea0f0e05004d9d5bfa6c293a2285d 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -1,6 +1,6 @@
 From stdpp Require Export strings.
 From iris.proofmode Require Import base tokens.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Inductive sel_pat :=
   | SelPure
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 2da6bf52c313438a7e58e496c8edcf4e6cbd0bcb..b2edc3b4c8181b4e7cf91479c559193b3254abb7 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,6 +1,6 @@
 From stdpp Require Export strings.
 From iris.proofmode Require Import base tokens.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Inductive goal_kind := GSpatial | GModal | GIntuitionistic.
 
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index cb3a34fbf48686d59737563b618a065be51c65c3..b7d075007d0f8b129785f27750eb11af79bcd1f2 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import base.
-Set Default Proof Using "Type".
+From iris Require Import options.
 
 Inductive token :=
   | TName : string → token