From 71abda4d8480fc6528a1617aedbadde59705747b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Jan 2017 17:50:02 +0100
Subject: [PATCH] make "make quick" quick by adding hints about the used
 section variables

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing
---
 theories/algebra/agree.v                        | 2 ++
 theories/algebra/auth.v                         | 1 +
 theories/algebra/base.v                         | 3 ++-
 theories/algebra/cmra.v                         | 1 +
 theories/algebra/cmra_big_op.v                  | 1 +
 theories/algebra/cmra_tactics.v                 | 1 +
 theories/algebra/coPset.v                       | 1 +
 theories/algebra/cofe_solver.v                  | 1 +
 theories/algebra/csum.v                         | 1 +
 theories/algebra/deprecated.v                   | 1 +
 theories/algebra/dra.v                          | 1 +
 theories/algebra/excl.v                         | 1 +
 theories/algebra/frac.v                         | 1 +
 theories/algebra/gmap.v                         | 1 +
 theories/algebra/gset.v                         | 1 +
 theories/algebra/iprod.v                        | 1 +
 theories/algebra/list.v                         | 1 +
 theories/algebra/local_updates.v                | 1 +
 theories/algebra/ofe.v                          | 1 +
 theories/algebra/sts.v                          | 1 +
 theories/algebra/updates.v                      | 1 +
 theories/algebra/vector.v                       | 1 +
 theories/base_logic/base_logic.v                | 1 +
 theories/base_logic/big_op.v                    | 1 +
 theories/base_logic/deprecated.v                | 1 +
 theories/base_logic/derived.v                   | 1 +
 theories/base_logic/double_negation.v           | 1 +
 theories/base_logic/hlist.v                     | 1 +
 theories/base_logic/lib/auth.v                  | 1 +
 theories/base_logic/lib/boxes.v                 | 1 +
 theories/base_logic/lib/cancelable_invariants.v | 1 +
 theories/base_logic/lib/core.v                  | 1 +
 theories/base_logic/lib/counter_examples.v      | 1 +
 theories/base_logic/lib/fancy_updates.v         | 1 +
 theories/base_logic/lib/fractional.v            | 1 +
 theories/base_logic/lib/gen_heap.v              | 1 +
 theories/base_logic/lib/invariants.v            | 1 +
 theories/base_logic/lib/iprop.v                 | 1 +
 theories/base_logic/lib/na_invariants.v         | 1 +
 theories/base_logic/lib/namespaces.v            | 1 +
 theories/base_logic/lib/own.v                   | 1 +
 theories/base_logic/lib/saved_prop.v            | 1 +
 theories/base_logic/lib/sts.v                   | 1 +
 theories/base_logic/lib/viewshifts.v            | 1 +
 theories/base_logic/lib/wsat.v                  | 1 +
 theories/base_logic/primitive.v                 | 1 +
 theories/base_logic/soundness.v                 | 1 +
 theories/base_logic/tactics.v                   | 1 +
 theories/base_logic/upred.v                     | 1 +
 theories/heap_lang/adequacy.v                   | 1 +
 theories/heap_lang/lang.v                       | 1 +
 theories/heap_lang/lib/assert.v                 | 1 +
 theories/heap_lang/lib/barrier/barrier.v        | 1 +
 theories/heap_lang/lib/barrier/proof.v          | 1 +
 theories/heap_lang/lib/barrier/protocol.v       | 1 +
 theories/heap_lang/lib/barrier/specification.v  | 1 +
 theories/heap_lang/lib/counter.v                | 1 +
 theories/heap_lang/lib/lock.v                   | 1 +
 theories/heap_lang/lib/par.v                    | 1 +
 theories/heap_lang/lib/spawn.v                  | 1 +
 theories/heap_lang/lib/spin_lock.v              | 1 +
 theories/heap_lang/lib/ticket_lock.v            | 1 +
 theories/heap_lang/lifting.v                    | 1 +
 theories/heap_lang/notation.v                   | 1 +
 theories/heap_lang/proofmode.v                  | 1 +
 theories/heap_lang/tactics.v                    | 1 +
 theories/prelude/base.v                         | 1 +
 theories/prelude/bset.v                         | 1 +
 theories/prelude/coPset.v                       | 1 +
 theories/prelude/collections.v                  | 1 +
 theories/prelude/countable.v                    | 1 +
 theories/prelude/decidable.v                    | 1 +
 theories/prelude/fin_collections.v              | 1 +
 theories/prelude/fin_map_dom.v                  | 1 +
 theories/prelude/fin_maps.v                     | 1 +
 theories/prelude/finite.v                       | 1 +
 theories/prelude/functions.v                    | 1 +
 theories/prelude/gmap.v                         | 1 +
 theories/prelude/gmultiset.v                    | 1 +
 theories/prelude/hashset.v                      | 1 +
 theories/prelude/hlist.v                        | 1 +
 theories/prelude/lexico.v                       | 1 +
 theories/prelude/list.v                         | 1 +
 theories/prelude/listset.v                      | 1 +
 theories/prelude/listset_nodup.v                | 1 +
 theories/prelude/mapset.v                       | 1 +
 theories/prelude/natmap.v                       | 1 +
 theories/prelude/nmap.v                         | 1 +
 theories/prelude/numbers.v                      | 1 +
 theories/prelude/option.v                       | 1 +
 theories/prelude/orders.v                       | 1 +
 theories/prelude/pmap.v                         | 1 +
 theories/prelude/pretty.v                       | 1 +
 theories/prelude/proof_irrel.v                  | 1 +
 theories/prelude/relations.v                    | 1 +
 theories/prelude/set.v                          | 3 ++-
 theories/prelude/sorting.v                      | 1 +
 theories/prelude/streams.v                      | 1 +
 theories/prelude/stringmap.v                    | 1 +
 theories/prelude/strings.v                      | 1 +
 theories/prelude/tactics.v                      | 1 +
 theories/prelude/vector.v                       | 1 +
 theories/prelude/zmap.v                         | 1 +
 theories/program_logic/adequacy.v               | 1 +
 theories/program_logic/ectx_language.v          | 1 +
 theories/program_logic/ectx_lifting.v           | 1 +
 theories/program_logic/ectxi_language.v         | 1 +
 theories/program_logic/hoare.v                  | 1 +
 theories/program_logic/language.v               | 1 +
 theories/program_logic/lifting.v                | 1 +
 theories/program_logic/ownp.v                   | 1 +
 theories/program_logic/weakestpre.v             | 1 +
 theories/proofmode/class_instances.v            | 1 +
 theories/proofmode/classes.v                    | 1 +
 theories/proofmode/coq_tactics.v                | 1 +
 theories/proofmode/environments.v               | 1 +
 theories/proofmode/intro_patterns.v             | 1 +
 theories/proofmode/notation.v                   | 1 +
 theories/proofmode/sel_patterns.v               | 1 +
 theories/proofmode/spec_patterns.v              | 1 +
 theories/proofmode/strings.v                    | 1 +
 theories/proofmode/tactics.v                    | 1 +
 theories/tests/barrier_client.v                 | 1 +
 theories/tests/counter.v                        | 1 +
 theories/tests/heap_lang.v                      | 1 +
 theories/tests/joining_existentials.v           | 1 +
 theories/tests/list_reverse.v                   | 1 +
 theories/tests/one_shot.v                       | 1 +
 theories/tests/proofmode.v                      | 1 +
 theories/tests/tree_sum.v                       | 1 +
 130 files changed, 133 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index acf7bdd5e..6353644d8 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 daa508e25..42cfa073a 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 483d63d72..77fdad017 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 f75552747..c35fac890 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 5c34694b7..12448601e 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 cdb25704a..08645cf32 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 b3e8f48d9..0f48c62fd 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 b304dbb42..84cb0b758 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 1adde00f7..b8d3bb359 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 45024d71d..0d3c5b62a 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 6bd0f0180..d79ad7928 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 a90fbd97d..ecb517229 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 bc9f469df..ee5cd143e 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 e6e4d23a8..e140399ca 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 cfaae2c76..a0a97f6f1 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 dda02f67f..9744e1355 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 9fca91363..61f773f0b 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 7ed0d5d35..9f6dde631 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 c0cf52f36..6e201a889 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 d19e19749..b52eca914 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 cdb1fc2d9..dc7a42fe1 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 51acea33c..c390c1a19 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 79029f48e..0d84d12c3 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 a21e33523..2a995bab1 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 01ac00577..e873c0534 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 a72988e00..16746c06a 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 7a31c8d93..95598242b 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 e70bd6eac..26a01fa5e 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 0adf6f97a..8f1f42242 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 e6a3b0f62..4e76e7d12 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 08a3e348b..c7f55710e 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 219e758b6..1bef3566a 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 be5b0b121..f325fc8e6 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 b291ecd52..c5d70fb17 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 49a856103..3f39eda43 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 a84e52a1f..7579343d6 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 8e0b12ef4..c8b647972 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 2c16ae741..730e8b518 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 61d22f6f0..9a72acc20 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 0b958278f..970b1ee9e 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 7a6ce609a..f1f3c4d0c 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 462a4762d..e0c8f2150 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 f3f5153a1..9fd943628 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 151bf0c50..aecea9568 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 c456f19f2..ae74942b2 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 0a6c7239e..db9f2b6b7 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 b2c7d8abf..a9f04c1e1 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 88a28ec8c..040d0ce77 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 5266c9ca1..944e5de7f 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 cfc7e1b41..c1d938a6f 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 4ef9b4c8d..6a8cc104c 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 511460f28..3569ae28c 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 61f8f7252..311ec5032 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 ee7d8d10c..00d731b55 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 e347613a1..c49a260df 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 a733cb1e1..7af0c8f21 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 45dcdf8aa..2923d524a 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 67f133851..9780eef82 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 2fcad149b..571308047 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 ab8d39d93..dd11ffaa5 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 77a7dbbaa..9349d0c1d 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 477a28442..2b6889920 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 9d3dfeb8f..e7fe25ded 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 58ca9a1b2..d36311eac 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 595b35c78..38eb5ed83 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 47d495d0e..11ae6e41e 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 51dcdad2f..859c6f009 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 92a6f2262..a431ca3cf 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 821504c54..0ad02732d 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 186673d47..f85aeba06 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 ef4b44b9a..aa8ae1b3c 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 ec5e19c4b..95e368550 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 7a26344f6..3936bde2f 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 3a657eb43..2ab691e22 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 34006bcb6..486ce36cd 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 3f4d0dd97..7109bf3a7 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 113ce19ec..da46a43a4 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 20faae2cb..4e5d2f774 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 c9e6d38bd..7782da245 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 dea9c7c02..dcfd1dfe3 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 386cc4206..907864fef 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 48880234d..6a7b868a3 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 ecf9fdac4..8ef98f665 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 7987bf223..a3fa10bad 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 25843624e..b9aedede3 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 20b5b6e6d..89417c054 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 f3491a1c1..b6e78446d 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 19bc574c7..0c965df3c 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 860ae09b7..c8eacf886 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 66fe22107..242ad4f5f 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 b3856cee4..9e6e2ca20 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 a8edba1cb..60ded55a1 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 1514dbc82..06924729b 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 892a9213c..b40985462 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 cf79ffee0..798245df8 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 0a96963fb..7e9385e80 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 aca5122e0..501c369f5 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 130510c01..1c9ef9aa9 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 c9f23a1e2..41fc9b8cb 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 3064d39d8..dca3404c1 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 bb13648f2..21d0122a1 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 4e62f4bcc..4b3426458 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 0d2cea6d4..c9c175919 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 43a0b12e0..9951b8e47 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 b86522443..76b2b167b 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 2011826e6..e27cd15d5 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 ec3aea0e5..74da06afc 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 f494db58c..b5ca5a347 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 de0d0a0c3..9c87c1e94 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 21b48a27a..b56edc556 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 4a22198dd..e57910e9f 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 31d3d48dc..b75cb874b 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 2e699f155..d246dd8a1 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 ed2689753..26cdd99aa 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 63e5989af..b252263d3 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 ebd7262f2..371381041 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 42760a8f8..a15af76ea 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 cde1ce716..d563702fc 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 4a77f4f08..9bc9c8ca6 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 d482d245b..92bd0c6b0 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 84d02cf67..3ed004744 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 74801c97c..d5c577970 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 eabcb4ca9..9490c527b 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 291ed8f14..baa9d394b 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 8e3c473c7..733b38f27 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 ecf84402c..cbf39efb3 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 77846047e..0a9943a50 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 8c1d21336..d657830c3 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 9e8e37be3..8f8479684 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 ebca3662f..09d317816 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
-- 
GitLab