From e252709ef747c1ff137cc6d9045a1ad9a7713442 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Aug 2020 18:44:31 +0200
Subject: [PATCH] use options file everywhere that we so far set 'Proof using'

---
 theories/algebra/agree.v                         | 4 ++--
 theories/algebra/auth.v                          | 2 +-
 theories/algebra/base.v                          | 2 +-
 theories/algebra/cmra.v                          | 2 +-
 theories/algebra/coPset.v                        | 2 +-
 theories/algebra/cofe_solver.v                   | 2 +-
 theories/algebra/csum.v                          | 2 +-
 theories/algebra/dra.v                           | 2 +-
 theories/algebra/excl.v                          | 2 +-
 theories/algebra/frac.v                          | 2 +-
 theories/algebra/functions.v                     | 2 +-
 theories/algebra/gmap.v                          | 2 +-
 theories/algebra/gmultiset.v                     | 2 +-
 theories/algebra/gset.v                          | 2 +-
 theories/algebra/list.v                          | 2 +-
 theories/algebra/local_updates.v                 | 2 +-
 theories/algebra/monoid.v                        | 2 +-
 theories/algebra/namespace_map.v                 | 2 +-
 theories/algebra/ofe.v                           | 2 +-
 theories/algebra/sts.v                           | 2 +-
 theories/algebra/ufrac.v                         | 2 +-
 theories/algebra/updates.v                       | 2 +-
 theories/algebra/vector.v                        | 2 +-
 theories/base_logic/base_logic.v                 | 2 +-
 theories/base_logic/derived.v                    | 2 +-
 theories/base_logic/lib/auth.v                   | 2 +-
 theories/base_logic/lib/boxes.v                  | 2 +-
 theories/base_logic/lib/cancelable_invariants.v  | 2 +-
 theories/base_logic/lib/fancy_updates.v          | 2 +-
 theories/base_logic/lib/gen_heap.v               | 2 +-
 theories/base_logic/lib/gen_inv_heap.v           | 2 +-
 theories/base_logic/lib/invariants.v             | 2 +-
 theories/base_logic/lib/iprop.v                  | 2 +-
 theories/base_logic/lib/na_invariants.v          | 2 +-
 theories/base_logic/lib/own.v                    | 2 +-
 theories/base_logic/lib/proph_map.v              | 2 +-
 theories/base_logic/lib/saved_prop.v             | 2 +-
 theories/base_logic/lib/sts.v                    | 2 +-
 theories/base_logic/lib/viewshifts.v             | 2 +-
 theories/base_logic/lib/wsat.v                   | 2 +-
 theories/base_logic/upred.v                      | 2 +-
 theories/bi/bi.v                                 | 2 +-
 theories/bi/big_op.v                             | 2 +-
 theories/bi/lib/atomic.v                         | 2 +-
 theories/bi/lib/core.v                           | 2 +-
 theories/bi/lib/fractional.v                     | 2 +-
 theories/bi/lib/laterable.v                      | 2 +-
 theories/bi/tactics.v                            | 2 +-
 theories/heap_lang/adequacy.v                    | 2 +-
 theories/heap_lang/derived_laws.v                | 2 +-
 theories/heap_lang/lang.v                        | 2 +-
 theories/heap_lang/lib/arith.v                   | 2 +-
 theories/heap_lang/lib/array.v                   | 2 +-
 theories/heap_lang/lib/assert.v                  | 2 +-
 theories/heap_lang/lib/atomic_heap.v             | 2 +-
 theories/heap_lang/lib/counter.v                 | 2 +-
 theories/heap_lang/lib/diverge.v                 | 2 +-
 theories/heap_lang/lib/increment.v               | 2 +-
 theories/heap_lang/lib/lock.v                    | 2 +-
 theories/heap_lang/lib/par.v                     | 2 +-
 theories/heap_lang/lib/spawn.v                   | 2 +-
 theories/heap_lang/lib/spin_lock.v               | 2 +-
 theories/heap_lang/lib/ticket_lock.v             | 2 +-
 theories/heap_lang/notation.v                    | 2 +-
 theories/heap_lang/primitive_laws.v              | 2 +-
 theories/heap_lang/proofmode.v                   | 2 +-
 theories/heap_lang/tactics.v                     | 2 +-
 theories/heap_lang/total_adequacy.v              | 2 +-
 theories/program_logic/adequacy.v                | 2 +-
 theories/program_logic/atomic.v                  | 2 +-
 theories/program_logic/ectx_language.v           | 2 +-
 theories/program_logic/ectx_lifting.v            | 2 +-
 theories/program_logic/ectxi_language.v          | 2 +-
 theories/program_logic/hoare.v                   | 2 +-
 theories/program_logic/language.v                | 2 +-
 theories/program_logic/lifting.v                 | 2 +-
 theories/program_logic/ownp.v                    | 2 +-
 theories/program_logic/total_adequacy.v          | 2 +-
 theories/program_logic/total_ectx_lifting.v      | 2 +-
 theories/program_logic/total_lifting.v           | 2 +-
 theories/program_logic/total_weakestpre.v        | 2 +-
 theories/program_logic/weakestpre.v              | 2 +-
 theories/proofmode/base.v                        | 2 +-
 theories/proofmode/class_instances.v             | 2 +-
 theories/proofmode/class_instances_embedding.v   | 2 +-
 theories/proofmode/class_instances_internal_eq.v | 2 +-
 theories/proofmode/class_instances_later.v       | 2 +-
 theories/proofmode/class_instances_plainly.v     | 2 +-
 theories/proofmode/class_instances_updates.v     | 2 +-
 theories/proofmode/classes.v                     | 2 +-
 theories/proofmode/coq_tactics.v                 | 2 +-
 theories/proofmode/environments.v                | 2 +-
 theories/proofmode/frame_instances.v             | 2 +-
 theories/proofmode/intro_patterns.v              | 2 +-
 theories/proofmode/ltac_tactics.v                | 2 +-
 theories/proofmode/modalities.v                  | 2 +-
 theories/proofmode/modality_instances.v          | 2 +-
 theories/proofmode/notation.v                    | 2 +-
 theories/proofmode/sel_patterns.v                | 2 +-
 theories/proofmode/spec_patterns.v               | 2 +-
 theories/proofmode/tokens.v                      | 2 +-
 101 files changed, 102 insertions(+), 102 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 332047646..d2783d6ec 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 8ae286844..8c6a51f9f 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 603e9c20c..3341e502c 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 b56fade14..a3d20798d 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 0cae57b57..2cff617b2 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 f5a190051..3fd8fe168 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 e6b483a42..5931a8850 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 9b58faaa1..1e8902001 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 a61d5e214..fcf4f879d 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 737208fd7..121c54296 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 893c56e0b..1d7353182 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 6e3b7311a..714a62663 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 6951db04b..701bb9d5a 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 eb7751229..b3a5d578c 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 50ceac0f1..5c94e79b6 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 199a7c16d..7a02bd42d 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 57e6a5efd..239d2d7fe 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 aaf7e2a71..7474b7e2c 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 c54e539c3..663f28440 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 5b4c19f5f..29682927c 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 42d9645d7..ed629c467 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 00462f7cb..b83285748 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 a72c887bb..dd904042e 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 13c4da994..d6fea5a09 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 01dff355c..b3f0cee87 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 d5d4ade21..a642742e6 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 eaea54618..a02be5297 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 234123b57..ab3325748 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 a98674442..ccd4ac39c 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 efe8eb9b2..3d57ed050 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 230ce9943..b371e4b06 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 4ddbe6895..adff4f6eb 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 214b72850..a40c6d1cf 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 00d4452b8..c99198241 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 ed77ef6f1..151572859 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 6793cd7a7..25391b5c9 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 ea836c510..648049114 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 05abc0e46..30ceaa110 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 d94376bc7..04b335836 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 1846c8912..b665b0562 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 fe44e0323..569746e0a 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 8f5aa1aa0..66afc4ad7 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 768a35757..1d0fd6e21 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 bea7c6639..d79d71a85 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 aa4001d33..dc67214dc 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 51253b19f..1721e6840 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 7983c6fb6..eaac68789 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 feb33d0fb..8881d03dc 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 bce15e435..56616ba1a 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 c2aafac5b..4a394f6b6 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 52616a5aa..d23eabdd2 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 bbaf8716d..501cfbabc 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 b41447205..8a16448b8 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 b8c932ef1..db8adb8d6 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 bdbc37838..f39fc9d07 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 2e41a5905..0cc86cfab 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 1a34a029c..393445f46 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 b479bc96a..bf71e6f3b 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 0430aec74..8edd581e4 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 a9378e599..fb33eb800 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 78bb22919..9b10f9247 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 33d4fa87f..1e5af4e73 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 311c7ae21..0947e7b54 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 6e60bbd0a..f9948af37 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 ecc290cff..5edc89f8f 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 f3280b9fc..d24214eb7 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 c3325b8dd..9b19bb9a6 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 8aa59f739..abb6118c7 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 a2bcf4e65..599c09a10 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 c035e92bc..13be0ce35 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 1894ba20e..774fe60df 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 7af252db4..926ae75c5 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 d647c618a..e9e9477c5 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 6eb2e36dc..b08d144fb 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 6999e0163..fb982fd7c 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 9a2d292e4..bb5fa43d6 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 7098222ab..0b5b33fc7 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 774dbf1d7..731f69079 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 9fe8e494e..99c34b6d3 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 eaf71db02..19b9af5a2 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 516043391..06f722a4f 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 8c2cb8f9a..e0d639fb6 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 e50c8c88d..abf4e1361 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 17ec680c2..2ee7a4d62 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 c7fd3a108..c75f27534 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 c33c76c79..c75ead317 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 bae07582c..1f850ff69 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 d7b20bb9e..f3eba370e 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 8a3f52152..9bc9f38aa 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 307c40349..50f03e157 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 871159211..72a33aa27 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 d9eea54a4..84713ce14 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 3e909d0b1..5a86fc7ca 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 1d3cb9922..d5895ebdc 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 203f53c92..92d12aacd 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 b4a5e0236..cc33f63bd 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 f586244c6..23d93c65e 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 0025dc12e..d2812ef7a 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 aac295086..0b360c196 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 2da6bf52c..b2edc3b4c 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 cb3a34fbf..b7d075007 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
-- 
GitLab