diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index acf7bdd5e58e57987b44627df06575720d40ded6..6353644d89fb0c5dc7a3575d302f67523046a985 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -1,6 +1,8 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import base_logic.
+(* FIXME: This file needs a 'Proof Using' hint. *)
+
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index daa508e25748c0430c3de1279986979ead6441fd..42cfa073ac41bdaa4ef6ef2d1894ffafdb9feaab 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export excl local_updates.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import classes.
+Set Default Proof Using "Type*".
 
 Record auth (A : Type) := Auth { authoritative : excl' A; auth_own : A }.
 Add Printing Constructor auth.
diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 483d63d721fa48c6111edc302facda9fee12731d..77fdad01703247c6cfba8e12041aded5c56fa891 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,5 +1,6 @@
 From mathcomp Require Export ssreflect.
 From iris.prelude Require Export prelude.
+Set Default Proof Using "Type*".
 Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.
-Ltac done := prelude.tactics.done.
\ No newline at end of file
+Ltac done := prelude.tactics.done.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index f75552747da6b23029bdb61df6bb70ab25d520f3..c35fac89001bc1b86b5afd8788ff50001ddcef30 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export ofe.
+Set Default Proof Using "Type*".
 
 Class PCore (A : Type) := pcore : A → option A.
 Instance: Params (@pcore) 2.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index 5c34694b7c4a965b52317fb5744a698ddfbca5e8..12448601ea5f605cdb272e963b81ea8b6f9a1966 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export cmra list.
 From iris.prelude Require Import functions gmap gmultiset.
+Set Default Proof Using "Type*".
 
 (** The operator [ [â‹…] Ps ] folds [â‹…] over the list [Ps]. This operator is not a
 quantifier, so it binds strongly.
diff --git a/theories/algebra/cmra_tactics.v b/theories/algebra/cmra_tactics.v
index cdb25704a60666625c1dfe7e9e83d0f66c4f3661..08645cf328b169c68f55b4ba751686df22c3d173 100644
--- a/theories/algebra/cmra_tactics.v
+++ b/theories/algebra/cmra_tactics.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import cmra_big_op.
+Set Default Proof Using "Type*".
 
 (** * Simple solver for validity and inclusion by reflection *)
 Module ra_reflection. Section ra_reflection.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index b3e8f48d943916dcad96b51eeaf5de2a86933853..0f48c62fd9a20f264e114d2b2e5c34b93c2b9e38 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections coPset.
+Set Default Proof Using "Type*".
 (** 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 b304dbb423f7a7408fbe6d6d436017ba7554cfb7..84cb0b75819b3c8efc34d4ea3fb4b7dd048e5ec7 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export ofe.
+Set Default Proof Using "Type*".
 
 Record solution (F : cFunctor) := Solution {
   solution_car :> ofeT;
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 1adde00f7fa2afa1e7337466174b75ccca88203d..b8d3bb35970b9f7d834fccfd98bf36c4999981a1 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import local_updates.
+Set Default Proof Using "Type*".
 Local Arguments pcore _ _ !_ /.
 Local Arguments cmra_pcore _ !_ /.
 Local Arguments validN _ _ _ !_ /.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 45024d71d45224bcb88f85f1861a5fcd54277f23..0d3c5b62adbef48a5ebde5327428df792a310700 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Import ofe cmra.
+Set Default Proof Using "Type*".
 
 (* Old notation for backwards compatibility. *)
 
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index 6bd0f018046f70561f4c0faa9ce55ce9754da56f..d79ad7928c3515c5a3762e19a9cc165183e8c913 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export cmra updates.
+Set Default Proof Using "Type*".
 
 Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   (* setoids *)
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index a90fbd97d60b644bd681af60640e72513918cde7..ecb517229f4ef1db68fa92201b637deab6aa5182 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
+Set Default Proof Using "Type*".
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index bc9f469df7e6915c242b84c11e94597f155401bc..ee5cd143e9cec6ee5184fa4c5c5d73241ae56ab5 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,5 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
+Set Default Proof Using "Type*".
 
 Notation frac := Qp (only parsing).
 
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index e6e4d23a8f2ac867cfd753fbe5b7deee608b3cb8..e140399cae69cb991ec7a2c607f9d5213376f582 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -2,6 +2,7 @@ From iris.algebra Require Export cmra.
 From iris.prelude Require Export gmap.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
+Set Default Proof Using "Type*".
 
 Section cofe.
 Context `{Countable K} {A : ofeT}.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index cfaae2c76fb1e9c0ba021652ba36327fce23c3f1..a0a97f6f1286ec7d748a12bb17713993f87eb6c3 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections gmap mapset.
+Set Default Proof Using "Type*".
 
 (* The union CMRA *)
 Section gset.
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index dda02f67fce96f07d70a0e89ad69a8645bcd60e5..9744e1355841672da6a8a9ba7585f20f517c8e9b 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From iris.prelude Require Import finite.
+Set Default Proof Using "Type*".
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 9fca913634bc6c90bfb01f2dde0714c5c59b4d80..61f773f0bd1ac20e6ec8c6e37854f5e0c25516c9 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -2,6 +2,7 @@ From iris.algebra Require Export cmra.
 From iris.prelude Require Export list.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
+Set Default Proof Using "Type*".
 
 Section cofe.
 Context {A : ofeT}.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 7ed0d5d35d4e991d981bf12cbc2fe553f8270058..9f6dde631dc38a7854a7a609796d2160bbb3d3d0 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export cmra.
+Set Default Proof Using "Type*".
 
 (** * Local updates *)
 Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c0cf52f3635fa0fffd1afb1cd500221dad4685bb..6e201a88958c3de7515bccc66b8a17e5e4aa261a 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export base.
+Set Default Proof Using "Type*".
 
 (** This files defines (a shallow embedding of) the category of OFEs:
     Complete ordered families of equivalences. This is a cartesian closed
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index d19e197490eec334037450f8d55cf673aaff89b8..b52eca914f52c8557b4cb034513315b4dd50cf41 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,6 +1,7 @@
 From iris.prelude Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
+Set Default Proof Using "Type*".
 Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments core _ _ !_ /.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index cdb1fc2d9fc1c00ab0f4de2a2918975f6f4db987..dc7a42fe10dc1bd6d862fd80b09e579e3437e1f3 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export cmra.
+Set Default Proof Using "Type*".
 
 (** * 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 51acea33caf43348befcd247414127eecdee8a6f..c390c1a19389b20250b82b756de3ae4b540e28af 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -1,6 +1,7 @@
 From iris.prelude Require Export vector.
 From iris.algebra Require Export ofe.
 From iris.algebra Require Import list.
+Set Default Proof Using "Type*".
 
 Section ofe.
   Context {A : ofeT}.
diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 79029f48e4b9a8e42f8c6d5d80a0f68906595959..0d84d12c3ce3804f4b8a548ddc4c442dd5216e0f 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,4 +1,5 @@
 From iris.base_logic Require Export derived.
+Set Default Proof Using "Type*".
 
 Module Import uPred.
   Export upred.uPred.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index a21e335232999815858404e062e9de732a4f42bb..2a995bab1a38062d9d2a05545aeabed7e5c7329d 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export list cmra_big_op.
 From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import gmap fin_collections gmultiset functions.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
diff --git a/theories/base_logic/deprecated.v b/theories/base_logic/deprecated.v
index 01ac005776b55ffc2a947e9a4ffe2bac17b9b9ce..e873c05341c7527274cdbdef7cb24f788c2ed8c1 100644
--- a/theories/base_logic/deprecated.v
+++ b/theories/base_logic/deprecated.v
@@ -1,4 +1,5 @@
 From iris.base_logic Require Import primitive.
+Set Default Proof Using "Type*".
 
 (* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
 Notation "■ φ" := (uPred_pure φ%C%type)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index a72988e00cb4791bb8a5d619970a5b743ea7d244..16746c06a5f5673cc9287d22b0756f97b3db4741 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,4 +1,5 @@
 From iris.base_logic Require Export primitive.
+Set Default Proof Using "Type*".
 Import upred.uPred primitive.uPred.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 7a31c8d93da90d3c014ea410f05bec5fd677eab9..95598242b5b314ca796fe94da904cad9898db1bc 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -1,4 +1,5 @@
 From iris.base_logic Require Import base_logic.
+Set Default Proof Using "Type*".
 
 (* In this file we show that the bupd can be thought of a kind of
    step-indexed double-negation when our meta-logic is classical *)
diff --git a/theories/base_logic/hlist.v b/theories/base_logic/hlist.v
index e70bd6eaca657453b93666772e022d2bd0fdb2ca..26a01fa5e7f3b42e23301f93b6f0c134ce75c4b2 100644
--- a/theories/base_logic/hlist.v
+++ b/theories/base_logic/hlist.v
@@ -1,5 +1,6 @@
 From iris.prelude Require Export hlist.
 From iris.base_logic Require Export base_logic.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 0adf6f97aa2e83f0f4e901da8c794fcf69f95f32..8f1f42242242b35b3ba194dde20cfd3eecc02df2 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -3,6 +3,7 @@ From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (* The CMRA we need. *)
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index e6a3b0f624cf1d4716c526b42fb973b1a2ce0ff6..4e76e7d12692879cde13cbf931061eba195d3d35 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -2,6 +2,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import auth gmap agree.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 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 08a3e348bdc8a99280edfa0e7f7bbe21d290b181..c7f55710e9d8ef9d5ce0ad6c680bcb76f79e1868 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,6 +1,7 @@
 From iris.base_logic.lib Require Export invariants fractional.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 219e758b6a1bc99a4ca0e83183ce6e8ba904de2f..1bef3566af60bbe861c9ed69a4212b7b017be5a6 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -1,5 +1,6 @@
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (** The "core" of an assertion is its maximal persistent part.
diff --git a/theories/base_logic/lib/counter_examples.v b/theories/base_logic/lib/counter_examples.v
index be5b0b12151831747b41bbdda328c4632f9253e5..f325fc8e60e38b16f2d5b1e07f62499524d1f395 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -1,5 +1,6 @@
 From iris.base_logic Require Import base_logic soundness.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "All".
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
 name-dependent allocation. *)
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index b291ecd52bf90526f009df389779dfde221d160e..c5d70fb1758d2c035341915f6e62d00922297022 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -4,6 +4,7 @@ From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
+Set Default Proof Using "Type*".
 Export invG.
 Import uPred.
 
diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v
index 49a856103799092a32ce4b34c6c9774905bb9e19..3f39eda433fc4c0d6117b0714b18561b0034a4d5 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -2,6 +2,7 @@ From iris.prelude Require Import gmap gmultiset.
 From iris.base_logic Require Export derived.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import classes class_instances.
+Set Default Proof Using "Type*".
 
 Class Fractional {M} (Φ : Qp → uPred M) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index a84e52a1f75b4163a2006fa9dea4156f8339e5e2..7579343d671ceef7e9345240c3bc67dcb3c57fc6 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -2,6 +2,7 @@ From iris.algebra Require Import auth gmap frac agree.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 8e0b12ef4fa68f1a290c37892c400d3dd24ea7ff..c8b6479728fe6935b937f3360355db66a94fdab3 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -2,6 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates namespaces.
 From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 2c16ae741412f1d8b226fa291285f76f7a59fa4c..730e8b518d0f92f350ea7ca94cbec5c25c9ad2c0 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,6 +1,7 @@
 From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import iprod gmap.
 From iris.algebra Require cofe_solver.
+Set Default Proof Using "Type*".
 
 (** 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 61d22f6f05681235f008e69a2657cb5f2f3ed710..9a72acc20579772f05288f7bb3aedfd1f5fa8077 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,6 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (* Non-atomic ("thread-local") invariants. *)
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index 0b958278f8747c92c1d459ad1f7a817bb504ecd7..970b1ee9e3430e4179d62a0c1fa6d25b192df510 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -1,5 +1,6 @@
 From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
+Set Default Proof Using "Type*".
 
 Definition namespace := list positive.
 Instance namespace_eq_dec : EqDecision namespace := _.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 7a6ce609afd972421057347923bf8482d6066c00..f1f3c4d0cafba2c36e14cb5729a0da78037f37be 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -2,6 +2,7 @@ From iris.algebra Require Import iprod gmap.
 From iris.base_logic Require Import big_op.
 From iris.base_logic Require Export iprop.
 From iris.proofmode Require Import classes.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 462a4762d6bb3c4d2ac6c7935fdce400f4b506b0..e0c8f2150dfd759aada97ff4a00dfc920a29aa6e 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,6 +1,7 @@
 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
 From iris.prelude Require Import gmap.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index f3f5153a1bd07e1895997f49b303d3f2a97a67a2..9fd9436285b06d551ff7c4afc6538a171b117c90 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,6 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (** The CMRA we need. *)
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 151bf0c5047faff6e5077658c3119cb01bcb5956..aecea9568b29c9d04ac275491441a952a4a86795 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -1,5 +1,6 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 
 Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P -∗ |={E1,E2}=> Q))%I.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index c456f19f24277e028eaa912739603b7a42ab2035..ae74942b2e2fb80cbd1bc2782d55606f1c289c5c 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -3,6 +3,7 @@ From iris.prelude Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 
 Module invG.
   Class invG (Σ : gFunctors) : Set := WsatG {
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 0a6c7239e5a53e0c0764d6864b77b84efaafedcb..db9f2b6b759db223a8d88f48cecc17d34a01f837 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -1,5 +1,6 @@
 From iris.base_logic Require Export upred.
 From iris.algebra Require Export updates.
+Set Default Proof Using "Type*".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
diff --git a/theories/base_logic/soundness.v b/theories/base_logic/soundness.v
index b2c7d8abf2e851601c7cda8d7ab1a61c1f1fb836..a9f04c1e1a4f9ae68e6f4814d839f4475e264e91 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -1,4 +1,5 @@
 From iris.base_logic Require Export base_logic.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Section adequacy.
diff --git a/theories/base_logic/tactics.v b/theories/base_logic/tactics.v
index 88a28ec8c2f0c313cb35eef6a8c93395055baa8b..040d0ce7793675c88355ddd7e0655b2dc71c8d9b 100644
--- a/theories/base_logic/tactics.v
+++ b/theories/base_logic/tactics.v
@@ -1,5 +1,6 @@
 From iris.prelude Require Import gmap.
 From iris.base_logic Require Export base_logic big_op.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Module uPred_reflection. Section uPred_reflection.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 5266c9ca12325425098982f92611bef4550ce5fa..944e5de7fb54d3e0baea8d1ce2f10619c581bd22 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export cmra.
+Set Default Proof Using "Type*".
 
 Record uPred (M : ucmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index cfc7e1b414219ac438a9bd6645efa7a941c44f57..c1d938a6f5e52e212cd6b0036ce294159f1b51fb 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -3,6 +3,7 @@ From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 4ef9b4c8dd16d0bedcde67decc9551683eb8e275..6a8cc104caa9e636668a3b9baba7af7d7e342b7f 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
+Set Default Proof Using "Type*".
 
 Module heap_lang.
 Open Scope Z_scope.
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index 511460f281cd053009262df410b36f115fd80b18..3569ae28c6aa4ef91dfa95dc85dd97885014db32 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type*".
 
 Definition assert : val :=
   λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
diff --git a/theories/heap_lang/lib/barrier/barrier.v b/theories/heap_lang/lib/barrier/barrier.v
index 61f8f72524eb58e09a144bf3e9683b80fea76657..311ec503219295ebd34802c68cef5749ec3be095 100644
--- a/theories/heap_lang/lib/barrier/barrier.v
+++ b/theories/heap_lang/lib/barrier/barrier.v
@@ -1,4 +1,5 @@
 From iris.heap_lang Require Export notation.
+Set Default Proof Using "Type*".
 
 Definition newbarrier : val := λ: <>, ref #false.
 Definition signal : val := λ: "x", "x" <- #true.
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index ee7d8d10c932c0c7d1d244b69707b2106be46208..00d731b5557d7ab1a291aa130cdaae83ac7f4bcd 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -5,6 +5,7 @@ From iris.prelude Require Import functions.
 From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.
+Set Default Proof Using "Type*".
 
 (** The CMRAs/functors we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
diff --git a/theories/heap_lang/lib/barrier/protocol.v b/theories/heap_lang/lib/barrier/protocol.v
index e347613a1c4e61af86826bb47c21a6cb748de97e..c49a260df38e0b0bd8d123379338305785147351 100644
--- a/theories/heap_lang/lib/barrier/protocol.v
+++ b/theories/heap_lang/lib/barrier/protocol.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Export sts.
 From iris.base_logic Require Import lib.own.
 From iris.prelude Require Export gmap.
+Set Default Proof Using "Type*".
 
 (** The STS describing the main barrier protocol. Every state has an index-set
     associated with it. These indices are actually [gname], because we use them
diff --git a/theories/heap_lang/lib/barrier/specification.v b/theories/heap_lang/lib/barrier/specification.v
index a733cb1e10e6a0806448e5278aac0068379d317d..7af0c8f21bf4f275984eb32fcb9a507e6af39c59 100644
--- a/theories/heap_lang/lib/barrier/specification.v
+++ b/theories/heap_lang/lib/barrier/specification.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export hoare.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import proofmode.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Section spec.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 45dcdf8aa0a6140200738b892d16c1201d715d0f..2923d524a0810659d4db2d6ce47196b052a366f4 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -4,6 +4,7 @@ From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac auth.
 From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type*".
 
 Definition newcounter : val := λ: <>, ref #0.
 Definition incr : val := rec: "incr" "l" :=
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index 67f1338512d502747c217e785bcb0a3db0cd69ed..9780eef8228f0a0e22d0ae8efbf9a807b3cc900e 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,5 +1,6 @@
 From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
+Set Default Proof Using "Type*".
 
 Structure lock Σ `{!heapG Σ} := Lock {
   (* -- operations -- *)
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 2fcad149b3ce6198c9a4fe01ff6ebabf7a296fd1..5713080475b6f81e7366f0462c203ab8fc40a858 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -1,5 +1,6 @@
 From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Definition parN : namespace := nroot .@ "par".
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index ab8d39d93b1a023cc6a94deae3cc75302c58dbd4..dd11ffaa5a0a7a8f4337ba7dc1dc9c77911c2d7b 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -4,6 +4,7 @@ From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
+Set Default Proof Using "Type*".
 
 Definition spawn : val :=
   λ: "f",
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 77a7dbbaa16d56830a44c18a39c57e053cbf79fb..9349d0c1d75dd1098e844349b244004880767857 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -4,6 +4,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl.
 From iris.heap_lang.lib Require Import lock.
+Set Default Proof Using "Type*".
 
 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 477a28442946089bc8ba37292949537839283448..2b68899209edc3d0867c5d4b932da44aac1086be 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -4,6 +4,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import auth gset.
 From iris.heap_lang.lib Require Export lock.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Definition wait_loop: val :=
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9d3dfeb8f934ef12463cd28c8804369ab5e342cb..e7fe25ded4ced40b5cd62f2e2816636f671c3a03 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -5,6 +5,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From iris.prelude Require Import fin_maps.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (** Basic rules for language operations. *)
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 58ca9a1b29c43cd90117112ec909931ff3c80b47..d36311eac2c7c7cf0d75f836972bbf69199f44a3 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -1,5 +1,6 @@
 From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang tactics.
+Set Default Proof Using "Type*".
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 595b35c7809d18da0b563268904db4311ff44d33..38eb5ed83f0d4a3615165e8dd6e51356a76cc84e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 47d495d0e110b600fc6987ef66c1e6921f1ff3c5..11ae6e41e6904466943670ea3f1b62cd3fd82a0a 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -1,4 +1,5 @@
 From iris.heap_lang Require Export lang.
+Set Default Proof Using "Type*".
 Import heap_lang.
 
 (** We define an alternative representation of expressions in which the
diff --git a/theories/prelude/base.v b/theories/prelude/base.v
index 51dcdad2f233e0fa907ac48a321b8dd648e4044d..859c6f009c545ee34b790e35bda610872105c3d9 100644
--- a/theories/prelude/base.v
+++ b/theories/prelude/base.v
@@ -9,6 +9,7 @@ Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
 Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+Set Default Proof Using "Type*".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 Obligation Tactic := idtac.
diff --git a/theories/prelude/bset.v b/theories/prelude/bset.v
index 92a6f22624250d92ceac57bae627859174e95759..a431ca3cfc713502d05f1e0038eab093e9731d22 100644
--- a/theories/prelude/bset.v
+++ b/theories/prelude/bset.v
@@ -2,6 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements bsets as functions into Prop. *)
 From iris.prelude Require Export prelude.
+Set Default Proof Using "Type*".
 
 Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
 Arguments mkBSet {_} _.
diff --git a/theories/prelude/coPset.v b/theories/prelude/coPset.v
index 821504c5403d6e67206919973bfc16285697ec52..0ad02732ddc81f2ab981ca3e29573792401c7d65 100644
--- a/theories/prelude/coPset.v
+++ b/theories/prelude/coPset.v
@@ -13,6 +13,7 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
 to the decision function that map bitstrings to bools. *)
 From iris.prelude Require Export collections.
 From iris.prelude Require Import pmap gmap mapset.
+Set Default Proof Using "Type*".
 Local Open Scope positive_scope.
 
 (** * The tree data structure *)
diff --git a/theories/prelude/collections.v b/theories/prelude/collections.v
index 186673d478693bfcb590c331a5b5b0ad2096c96b..f85aeba0664040b92d6d7b2deb205f18138fe86d 100644
--- a/theories/prelude/collections.v
+++ b/theories/prelude/collections.v
@@ -4,6 +4,7 @@
 importantly, it implements some tactics to automatically solve goals involving
 collections. *)
 From iris.prelude Require Export orders list.
+Set Default Proof Using "Type*".
 
 Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
diff --git a/theories/prelude/countable.v b/theories/prelude/countable.v
index ef4b44b9a11b3acab1d53940fa63026f62193911..aa8ae1b3cdc5082645de6124f874dd5548c99841 100644
--- a/theories/prelude/countable.v
+++ b/theories/prelude/countable.v
@@ -1,6 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Export list.
+Set Default Proof Using "Type*".
 Local Open Scope positive.
 
 Class Countable A `{EqDecision A} := {
diff --git a/theories/prelude/decidable.v b/theories/prelude/decidable.v
index ec5e19c4b717f5e05ddddf55bea4d30a86e246f5..95e368550bfe15ef7ae8f58fa859c6b9c1541ca0 100644
--- a/theories/prelude/decidable.v
+++ b/theories/prelude/decidable.v
@@ -4,6 +4,7 @@
 with a decidable equality. Such propositions are collected by the [Decision]
 type class. *)
 From iris.prelude Require Export proof_irrel.
+Set Default Proof Using "Type*".
 
 Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
 
diff --git a/theories/prelude/fin_collections.v b/theories/prelude/fin_collections.v
index 7a26344f671cda69e9bb0c87c8abd759d96fa65a..3936bde2fcd662569e33295316897979a7aa4b84 100644
--- a/theories/prelude/fin_collections.v
+++ b/theories/prelude/fin_collections.v
@@ -6,6 +6,7 @@ principles on finite collections . *)
 From Coq Require Import Permutation.
 From iris.prelude Require Import relations listset.
 From iris.prelude Require Export numbers collections.
+Set Default Proof Using "Type*".
 
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
 Definition collection_fold `{Elements A C} {B}
diff --git a/theories/prelude/fin_map_dom.v b/theories/prelude/fin_map_dom.v
index 3a657eb433436f942547b35dabba6f4279bb38c4..2ab691e22f2702b5e9104bdd1cb8d0e009e9e99b 100644
--- a/theories/prelude/fin_map_dom.v
+++ b/theories/prelude/fin_map_dom.v
@@ -4,6 +4,7 @@
 maps. We provide such an axiomatization, instead of implementing the domain
 function in a generic way, to allow more efficient implementations. *)
 From iris.prelude Require Export collections fin_maps.
+Set Default Proof Using "Type*".
 
 Class FinMapDom K M D `{FMap M,
     ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
diff --git a/theories/prelude/fin_maps.v b/theories/prelude/fin_maps.v
index 34006bcb608d7b546712c6cb9a794ea30c9ea681..486ce36cdd5ffefe8b566fffb245a3569c872cf2 100644
--- a/theories/prelude/fin_maps.v
+++ b/theories/prelude/fin_maps.v
@@ -6,6 +6,7 @@ induction principles for finite maps and implements the tactic
 [simplify_map_eq] to simplify goals involving finite maps. *)
 From Coq Require Import Permutation.
 From iris.prelude Require Export relations orders vector.
+Set Default Proof Using "Type*".
 
 (** * Axiomatization of finite maps *)
 (** We require Leibniz equality to be extensional on finite maps. This of
diff --git a/theories/prelude/finite.v b/theories/prelude/finite.v
index 3f4d0dd97b2f8dad0aec3425fe83ab8752d3c60d..7109bf3a7dceef7308a830dccee6c3f8876f6864 100644
--- a/theories/prelude/finite.v
+++ b/theories/prelude/finite.v
@@ -1,6 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Export countable vector.
+Set Default Proof Using "Type*".
 
 Class Finite A `{EqDecision A} := {
   enum : list A;
diff --git a/theories/prelude/functions.v b/theories/prelude/functions.v
index 113ce19ec54634321b599a881ad8b084f9540088..da46a43a468911e654cd1b3ad5e63eda4876f353 100644
--- a/theories/prelude/functions.v
+++ b/theories/prelude/functions.v
@@ -1,4 +1,5 @@
 From iris.prelude Require Export base tactics.
+Set Default Proof Using "Type*".
 
 Section definitions.
   Context {A T : Type} `{EqDecision A}.
diff --git a/theories/prelude/gmap.v b/theories/prelude/gmap.v
index 20faae2cb97d47071a72ed55f7891de6a26aba06..4e5d2f7746cdea3be3aef26871052ca5a49b2d1f 100644
--- a/theories/prelude/gmap.v
+++ b/theories/prelude/gmap.v
@@ -4,6 +4,7 @@
 type. The implementation is based on [Pmap]s, radix-2 search trees. *)
 From iris.prelude Require Export countable fin_maps fin_map_dom.
 From iris.prelude Require Import pmap mapset set.
+Set Default Proof Using "Type*".
 
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
diff --git a/theories/prelude/gmultiset.v b/theories/prelude/gmultiset.v
index c9e6d38bdf763061919cf27c72f6c262d8bedfd8..7782da2455494db701aa985a4b0840b5f6060b4b 100644
--- a/theories/prelude/gmultiset.v
+++ b/theories/prelude/gmultiset.v
@@ -1,6 +1,7 @@
 (* Copyright (c) 2012-2016, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Import gmap.
+Set Default Proof Using "Type*".
 
 Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
 Arguments GMultiSet {_ _ _} _.
diff --git a/theories/prelude/hashset.v b/theories/prelude/hashset.v
index dea9c7c02db921c691d363e8e51cc0bd7738baa3..dcfd1dfe38084e94a4db0106f0f7a5b27ee52da9 100644
--- a/theories/prelude/hashset.v
+++ b/theories/prelude/hashset.v
@@ -5,6 +5,7 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary
 integer of type [Z], and contains an unordered list without duplicates. *)
 From iris.prelude Require Export fin_maps listset.
 From iris.prelude Require Import zmap.
+Set Default Proof Using "Type*".
 
 Record hashset {A} (hash : A → Z) := Hashset {
   hashset_car : Zmap (list A);
diff --git a/theories/prelude/hlist.v b/theories/prelude/hlist.v
index 386cc42066800d3ca7986b4521f49102dc2db8a0..907864fef88284a254f9ef075ff4979a622102f0 100644
--- a/theories/prelude/hlist.v
+++ b/theories/prelude/hlist.v
@@ -1,4 +1,5 @@
 From iris.prelude Require Import tactics.
+Set Default Proof Using "Type*".
 Local Set Universe Polymorphism.
 
 (* Not using [list Type] in order to avoid universe inconsistencies *)
diff --git a/theories/prelude/lexico.v b/theories/prelude/lexico.v
index 48880234ddb18229a8de46a003a14c9849e4c9c6..6a7b868a34c36033fa9abe9e3d12f5b3e605090e 100644
--- a/theories/prelude/lexico.v
+++ b/theories/prelude/lexico.v
@@ -3,6 +3,7 @@
 (** This files defines a lexicographic order on various common data structures
 and proves that it is a partial order having a strong variant of trichotomy. *)
 From iris.prelude Require Import numbers.
+Set Default Proof Using "Type*".
 
 Notation cast_trichotomy T :=
   match T with
diff --git a/theories/prelude/list.v b/theories/prelude/list.v
index ecf9fdac4a5a3ff9328a9eced060f642c57b301e..8ef98f665e3e9bd0f386ff9cfbbe1df2332215f1 100644
--- a/theories/prelude/list.v
+++ b/theories/prelude/list.v
@@ -4,6 +4,7 @@
 are not in the Coq standard library. *)
 From Coq Require Export Permutation.
 From iris.prelude Require Export numbers base option.
+Set Default Proof Using "Type*".
 
 Arguments length {_} _.
 Arguments cons {_} _ _.
diff --git a/theories/prelude/listset.v b/theories/prelude/listset.v
index 7987bf223cae39d5c8fc768a8b72361b3db1fc9d..a3fa10badd7fc78430b96f36106a20ae7133f3b8 100644
--- a/theories/prelude/listset.v
+++ b/theories/prelude/listset.v
@@ -3,6 +3,7 @@
 (** This file implements finite set as unordered lists without duplicates
 removed. This implementation forms a monad. *)
 From iris.prelude Require Export collections list.
+Set Default Proof Using "Type*".
 
 Record listset A := Listset { listset_car: list A }.
 Arguments listset_car {_} _.
diff --git a/theories/prelude/listset_nodup.v b/theories/prelude/listset_nodup.v
index 25843624ef383e66b0f7b000b3b89b853e58b9ba..b9aedede369f901865088713eea5127f3b042f4f 100644
--- a/theories/prelude/listset_nodup.v
+++ b/theories/prelude/listset_nodup.v
@@ -4,6 +4,7 @@
 Although this implementation is slow, it is very useful as decidable equality
 is the only constraint on the carrier set. *)
 From iris.prelude Require Export collections list.
+Set Default Proof Using "Type*".
 
 Record listset_nodup A := ListsetNoDup {
   listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
diff --git a/theories/prelude/mapset.v b/theories/prelude/mapset.v
index 20b5b6e6dec8859c715974b8d59651927082f01a..89417c0546aea2180d0711ba0b9e49c6284bf3c6 100644
--- a/theories/prelude/mapset.v
+++ b/theories/prelude/mapset.v
@@ -4,6 +4,7 @@
 elements of the unit type. Since maps enjoy extensional equality, the
 constructed finite sets do so as well. *)
 From iris.prelude Require Export fin_map_dom.
+(* FIXME: This file needs a 'Proof Using' hint. *)
 
 Record mapset (M : Type → Type) : Type :=
   Mapset { mapset_car: M (unit : Type) }.
diff --git a/theories/prelude/natmap.v b/theories/prelude/natmap.v
index f3491a1c16857f5c6a0adeff75deef8c6a9ef805..b6e78446d5fc8626faec5077db1a9c887846e04a 100644
--- a/theories/prelude/natmap.v
+++ b/theories/prelude/natmap.v
@@ -4,6 +4,7 @@
 over Coq's data type of unary natural numbers [nat]. The implementation equips
 a list with a proof of canonicity. *)
 From iris.prelude Require Import fin_maps mapset.
+Set Default Proof Using "Type*".
 
 Notation natmap_raw A := (list (option A)).
 Definition natmap_wf {A} (l : natmap_raw A) :=
diff --git a/theories/prelude/nmap.v b/theories/prelude/nmap.v
index 19bc574c71a884fba952ff80408b8e5c60325430..0c965df3cd7b7a3007f26a9ce279599d5b0b0748 100644
--- a/theories/prelude/nmap.v
+++ b/theories/prelude/nmap.v
@@ -4,6 +4,7 @@
 maps whose keys range over Coq's data type of binary naturals [N]. *)
 From iris.prelude Require Import pmap mapset.
 From iris.prelude Require Export prelude fin_maps.
+Set Default Proof Using "Type*".
 
 Local Open Scope N_scope.
 
diff --git a/theories/prelude/numbers.v b/theories/prelude/numbers.v
index 860ae09b796b3ec3390ddb3fd34c829385a34502..c8eacf886eabd5b113530ad6e00a5a85c7b05726 100644
--- a/theories/prelude/numbers.v
+++ b/theories/prelude/numbers.v
@@ -6,6 +6,7 @@ notations. *)
 From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
 From iris.prelude Require Export base decidable option.
+Set Default Proof Using "Type*".
 Open Scope nat_scope.
 
 Coercion Z.of_nat : nat >-> Z.
diff --git a/theories/prelude/option.v b/theories/prelude/option.v
index 66fe22107bdffb6c5baad967423adf6b7c036299..242ad4f5f96ae13ba630351b8564c2abee9ed0a5 100644
--- a/theories/prelude/option.v
+++ b/theories/prelude/option.v
@@ -3,6 +3,7 @@
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
 From iris.prelude Require Export tactics.
+Set Default Proof Using "Type*".
 
 Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type :=
   | ReflectSome x : P x → option_reflect P Q (Some x)
diff --git a/theories/prelude/orders.v b/theories/prelude/orders.v
index b3856cee4b01f7118bd12c01eddf720fcd09f840..9e6e2ca20ecf7245a4634d2b5adfc23aeef5addc 100644
--- a/theories/prelude/orders.v
+++ b/theories/prelude/orders.v
@@ -3,6 +3,7 @@
 (** Properties about arbitrary pre-, partial, and total orders. We do not use
 the relation [⊆] because we often have multiple orders on the same structure *)
 From iris.prelude Require Export tactics.
+Set Default Proof Using "Type*".
 
 Section orders.
   Context {A} {R : relation A}.
diff --git a/theories/prelude/pmap.v b/theories/prelude/pmap.v
index a8edba1cb6857840fcf33b53476b6a595c625620..60ded55a1d0e21c0e5f59ae0a4a6f199b56ea801 100644
--- a/theories/prelude/pmap.v
+++ b/theories/prelude/pmap.v
@@ -10,6 +10,7 @@ Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
 From iris.prelude Require Import mapset countable.
 From iris.prelude Require Export fin_maps.
+Set Default Proof Using "Type*".
 
 Local Open Scope positive_scope.
 Local Hint Extern 0 (@eq positive _ _) => congruence.
diff --git a/theories/prelude/pretty.v b/theories/prelude/pretty.v
index 1514dbc829a77081313670ed35028d5fa64596f8..06924729b0dc363cd6ee1b30d55d809c96660ff5 100644
--- a/theories/prelude/pretty.v
+++ b/theories/prelude/pretty.v
@@ -3,6 +3,7 @@
 From iris.prelude Require Export strings.
 From iris.prelude Require Import relations.
 From Coq Require Import Ascii.
+Set Default Proof Using "Type*".
 
 Class Pretty A := pretty : A → string.
 Definition pretty_N_char (x : N) : ascii :=
diff --git a/theories/prelude/proof_irrel.v b/theories/prelude/proof_irrel.v
index 892a9213c3d6ce39de3c94fad263708e53436d8e..b409854626c30804db5f1ae82938064c3e47cddc 100644
--- a/theories/prelude/proof_irrel.v
+++ b/theories/prelude/proof_irrel.v
@@ -2,6 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects facts on proof irrelevant types/propositions. *)
 From iris.prelude Require Export base.
+Set Default Proof Using "Type*".
 
 Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
 
diff --git a/theories/prelude/relations.v b/theories/prelude/relations.v
index cf79ffee0e000a0fb1da467f21274aa61cee5bb4..798245df8fb37adc2a8138c0fd0de11752cfb9fa 100644
--- a/theories/prelude/relations.v
+++ b/theories/prelude/relations.v
@@ -6,6 +6,7 @@ small step semantics. This file defines a hint database [ars] containing
 some theorems on abstract rewriting systems. *)
 From Coq Require Import Wf_nat.
 From iris.prelude Require Export tactics base.
+Set Default Proof Using "Type*".
 
 (** * Definitions *)
 Section definitions.
diff --git a/theories/prelude/set.v b/theories/prelude/set.v
index 0a96963fbaebfb9f535d7c8823102194c433a5f3..7e9385e8096e1a5969e779135e5104d396979cb3 100644
--- a/theories/prelude/set.v
+++ b/theories/prelude/set.v
@@ -2,6 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements sets as functions into Prop. *)
 From iris.prelude Require Export collections.
+Set Default Proof Using "Type*".
 
 Record set (A : Type) : Type := mkSet { set_car : A → Prop }.
 Add Printing Constructor set.
@@ -51,4 +52,4 @@ Proof. intros HPQ. constructor. apply HPQ. Qed.
 
 Global Opaque set_elem_of set_top set_empty set_singleton.
 Global Opaque set_union set_intersection set_difference.
-Global Opaque set_ret set_bind set_fmap set_join.
\ No newline at end of file
+Global Opaque set_ret set_bind set_fmap set_join.
diff --git a/theories/prelude/sorting.v b/theories/prelude/sorting.v
index aca5122e060d55dd0843bf35b28c93c3e70366dd..501c369f5d005f671beaa1372977fc89c437b6c6 100644
--- a/theories/prelude/sorting.v
+++ b/theories/prelude/sorting.v
@@ -4,6 +4,7 @@
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
 From iris.prelude Require Export orders list.
+Set Default Proof Using "Type*".
 
 Section merge_sort.
   Context {A} (R : relation A) `{∀ x y, Decision (R x y)}.
diff --git a/theories/prelude/streams.v b/theories/prelude/streams.v
index 130510c016ce0b781988ab64d2405dc46423f6da..1c9ef9aa95f544b04ca7b4dbda7d5b9bfc4bdf93 100644
--- a/theories/prelude/streams.v
+++ b/theories/prelude/streams.v
@@ -1,6 +1,7 @@
 (* Copyright (c) 2012-2015, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Export tactics.
+Set Default Proof Using "Type*".
 
 CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
 Arguments scons {_} _ _.
diff --git a/theories/prelude/stringmap.v b/theories/prelude/stringmap.v
index c9f23a1e2cbf063906696bb2d6c5252c8990a4a2..41fc9b8cbcc8353a0ccb57014432c1a07a71ee22 100644
--- a/theories/prelude/stringmap.v
+++ b/theories/prelude/stringmap.v
@@ -6,6 +6,7 @@ search trees (uncompressed Patricia trees) as implemented in the file [pmap]
 and guarantees logarithmic-time operations. *)
 From iris.prelude Require Export fin_maps pretty.
 From iris.prelude Require Import gmap.
+Set Default Proof Using "Type*".
 
 Notation stringmap := (gmap string).
 Notation stringset := (gset string).
diff --git a/theories/prelude/strings.v b/theories/prelude/strings.v
index 3064d39d8402d6db524d2a1df4788b566a123567..dca3404c10e93169afc142ad2cb03d6ecc202697 100644
--- a/theories/prelude/strings.v
+++ b/theories/prelude/strings.v
@@ -4,6 +4,7 @@ From Coq Require Import Ascii.
 From Coq Require Export String.
 From iris.prelude Require Export list.
 From iris.prelude Require Import countable.
+Set Default Proof Using "Type*".
 
 (* To avoid randomly ending up with String.length because this module is
 imported hereditarily somewhere. *)
diff --git a/theories/prelude/tactics.v b/theories/prelude/tactics.v
index bb13648f2a496a7d429e17607e47122ae535c351..21d0122a1e4331438f3d2692d338f0bbfefab258 100644
--- a/theories/prelude/tactics.v
+++ b/theories/prelude/tactics.v
@@ -5,6 +5,7 @@ the development. *)
 From Coq Require Import Omega.
 From Coq Require Export Lia.
 From iris.prelude Require Export decidable.
+Set Default Proof Using "Type*".
 
 Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
 Proof. intros ->; reflexivity. Qed.
diff --git a/theories/prelude/vector.v b/theories/prelude/vector.v
index 4e62f4bcc1a12438045473b0ca4be7a8956d8846..4b34264582b455e6894fa705c7aaf29c8d7dcf93 100644
--- a/theories/prelude/vector.v
+++ b/theories/prelude/vector.v
@@ -6,6 +6,7 @@ definitions from the standard library, but renames or changes their notations,
 so that it becomes more consistent with the naming conventions in this
 development. *)
 From iris.prelude Require Export list.
+Set Default Proof Using "Type*".
 Open Scope vector_scope.
 
 (** * The fin type *)
diff --git a/theories/prelude/zmap.v b/theories/prelude/zmap.v
index 0d2cea6d4c19aaab0c4abccc0e6beeb50c5ca401..c9c1759196e8d53c45d850971e6b7ca81ae52cdb 100644
--- a/theories/prelude/zmap.v
+++ b/theories/prelude/zmap.v
@@ -4,6 +4,7 @@
 maps whose keys range over Coq's data type of binary naturals [Z]. *)
 From iris.prelude Require Import pmap mapset.
 From iris.prelude Require Export prelude fin_maps.
+Set Default Proof Using "Type*".
 Local Open Scope Z_scope.
 
 Record Zmap (A : Type) : Type :=
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 43a0b12e03cc31d76c2217977f6b79dfdff28a89..9951b8e479db26a6012ca72b11047c19a2beffba 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -3,6 +3,7 @@ From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 Import uPred.
 
 (* Global functor setup *)
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index b86522443e4c7b9b2ac6d73a504a9fda6cdb19c2..76b2b167bf94b3decd6c6330b0fc94a0649787af 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -2,6 +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*".
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 2011826e699d3f8602855b0d9949c9fb52b3f6e7..e27cd15d50d75143e24f795fb42ffcf947f541c6 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,6 +1,7 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index ec3aea0e5b15c2ac599f24b11c874e3e77624ed0..74da06afcedc81a80c5ed3c41527529cd02bc2fb 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -2,6 +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*".
 
 (* We need to make thos arguments indices that we want canonical structure
    inference to use a keys. *)
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index f494db58c8c718480f926e0bb6fa1b03012d5447..b5ca5a347f18a71591028738222c39f3d7bcb2d3 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index de0d0a0c395a2e781620ccdd13c70765e1c9c611..9c87c1e94ce3bf1f257c02d7247f619d993342d2 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Export ofe.
+Set Default Proof Using "Type*".
 
 Structure language := Language {
   expr : Type;
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 21b48a27aa2a00d4bf01212bda7b049d190a6aa9..b56edc5568a781bd99d14bc90cd987fdf000205f 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,6 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.base_logic Require Export big_op.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 
 Section lifting.
 Context `{irisG Λ Σ}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 4a22198ddaff984f338481b98e23c9c640246ebc..e57910e9fdd8f1e26e5b8949d6ee1470ac2cb0e7 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -3,6 +3,7 @@ From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
 From iris.algebra Require Import auth.
 From iris.proofmode Require Import tactics classes.
+Set Default Proof Using "Type*".
 
 Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 31d3d48dcfb20ec961339618b76dc948e341d25a..b75cb874b2c6be8efd1ac143caeda06e2d95ebdc 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -2,6 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 2e699f1550bdff85d865665328c6405558ecb8ea..d246dd8a174905001c676f23ddafcdab47907825 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Export classes.
 From iris.algebra Require Import gmap.
 From iris.prelude Require Import gmultiset.
 From iris.base_logic Require Import big_op.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Section classes.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index ed2689753698f7c0888ac1c0cbf81f2ae3822b8e..26cdd99aad16a922a3bb4c08447c15862084e552 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -1,4 +1,5 @@
 From iris.base_logic Require Export base_logic.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Section classes.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 63e5989af0d5b9c8fc569d2933bac3827c239c98..b252263d34b5c784382018b77ad4b7670afaa8af 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -2,6 +2,7 @@ From iris.base_logic Require Export base_logic.
 From iris.base_logic Require Import big_op tactics.
 From iris.proofmode Require Export environments classes.
 From iris.prelude Require Import stringmap hlist.
+Set Default Proof Using "Type*".
 Import uPred.
 Import env_notations.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index ebd7262f206b4d58c26ea5a7f29bfd27b56e32a7..371381041d745c149baf81048d95222be7917854 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -2,6 +2,7 @@ From iris.prelude Require Export strings.
 From iris.proofmode Require Import strings.
 From iris.algebra Require Export base.
 From iris.prelude Require Import stringmap.
+Set Default Proof Using "Type*".
 
 Inductive env (A : Type) : Type :=
   | Enil : env A
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 42760a8f817b1b4aee90fb4433b985acc412d987..a15af76ea4aa3a77615d9caf548f769bc7753ace 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,4 +1,5 @@
 From iris.prelude Require Export strings.
+Set Default Proof Using "Type*".
 
 Inductive intro_pat :=
   | IName : string → intro_pat
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index cde1ce71618589ab3c63b1c12d4edf1dbec452c9..d563702fc5c5524a82863f5f6bf3bd528f07cc88 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import coq_tactics environments.
 From iris.prelude Require Export strings.
+Set Default Proof Using "Type*".
 
 Delimit Scope proof_scope with env.
 Arguments Envs _ _%proof_scope _%proof_scope.
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 4a77f4f08c3542f829382d95ea41e3038e70a7a7..9bc9c8ca62b4987d2498188c2be4a62a60bc980b 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -1,4 +1,5 @@
 From iris.prelude Require Export strings.
+Set Default Proof Using "Type*".
 
 Inductive sel_pat :=
   | SelPure
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index d482d245bbe390e3cffefdbfd83fb76b76866176..92bd0c6b0b7021db41a8fc913af33f191d52e035 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,4 +1,5 @@
 From iris.prelude Require Export strings.
+Set Default Proof Using "Type*".
 
 Record spec_goal := SpecGoal {
   spec_goal_modal : bool;
diff --git a/theories/proofmode/strings.v b/theories/proofmode/strings.v
index 84d02cf6711d42c0159d8fa71bf836b035855a53..3ed004744a382bf9c7f4f672cc8c3f4f6bed2346 100644
--- a/theories/proofmode/strings.v
+++ b/theories/proofmode/strings.v
@@ -1,6 +1,7 @@
 From iris.prelude Require Import strings.
 From iris.algebra Require Import base.
 From Coq Require Import Ascii.
+Set Default Proof Using "Type*".
 
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 74801c97c7c7d635bd244e22a9a24693b90d9892..d5c5779700a126f27da339fabe047c935dcd8665 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -5,6 +5,7 @@ From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From iris.prelude Require Import stringmap hlist.
 From iris.proofmode Require Import strings.
+Set Default Proof Using "Type*".
 
 Declare Reduction env_cbv := cbv [
   beq ascii_beq string_beq
diff --git a/theories/tests/barrier_client.v b/theories/tests/barrier_client.v
index eabcb4ca9d695d061a35885d67f1eacdf63f44fa..9490c527bd6eec95190f6edb915d5a07b92aee99 100644
--- a/theories/tests/barrier_client.v
+++ b/theories/tests/barrier_client.v
@@ -3,6 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Import proof.
 From iris.heap_lang Require Import par.
 From iris.heap_lang Require Import adequacy proofmode.
+Set Default Proof Using "Type*".
 
 Definition worker (n : Z) : val :=
   λ: "b" "y", wait "b" ;; !"y" #n.
diff --git a/theories/tests/counter.v b/theories/tests/counter.v
index 291ed8f1460c5546b63135098e5d3c1262f84ebd..baa9d394b10cef02912f2c852e025aa752df2fd1 100644
--- a/theories/tests/counter.v
+++ b/theories/tests/counter.v
@@ -8,6 +8,7 @@ From iris.heap_lang Require Export lang.
 From iris.program_logic Require Export hoare.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type*".
 Import uPred.
 
 Definition newcounter : val := λ: <>, ref #0.
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 8e3c473c7cb22e0f4f8ec159d9703d44a1a973e2..733b38f27461670d9f003db5bbc23807c1979de3 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -3,6 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
 From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type*".
 
 Section LiftingTests.
   Context `{heapG Σ}.
diff --git a/theories/tests/joining_existentials.v b/theories/tests/joining_existentials.v
index ecf84402c7ea78f1c3f478f1e207165b88995893..cbf39efb30b7cfb04f338c64898bcc152d390e86 100644
--- a/theories/tests/joining_existentials.v
+++ b/theories/tests/joining_existentials.v
@@ -4,6 +4,7 @@ From iris.algebra Require Import excl agree csum.
 From iris.heap_lang.lib.barrier Require Import proof specification.
 From iris.heap_lang Require Import notation par proofmode.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "All".
 
 Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
   csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
diff --git a/theories/tests/list_reverse.v b/theories/tests/list_reverse.v
index 77846047e054131907e71de989ed2cac47e9a3e7..0a9943a50b0192c822a9e10a48da60a7cc85ce0f 100644
--- a/theories/tests/list_reverse.v
+++ b/theories/tests/list_reverse.v
@@ -3,6 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type*".
 
 Section list_reverse.
 Context `{!heapG Σ}.
diff --git a/theories/tests/one_shot.v b/theories/tests/one_shot.v
index 8c1d21336ffb1dafa0a3852c4f840e72554d0b48..d657830c3183513b8ad44a5dbb0312446503466d 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -3,6 +3,7 @@ From iris.heap_lang Require Export lang.
 From iris.algebra Require Import excl agree csum.
 From iris.heap_lang Require Import assert proofmode notation.
 From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type*".
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 9e8e37be3adee535af4b05a800058d7b6bb2ab9f..8f8479684460c5e5b88f4e6b787ad43a42953c76 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -1,5 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
+Set Default Proof Using "Type*".
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
   □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index ebca3662f90260bd0416c5ad814aa957d75c76da..09d3178162237243890b15617bf33c7d3e556ec5 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type*".
 
 Inductive tree :=
   | leaf : Z → tree