diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 11cf3fb3011afea6ba88ecc2dbb85ab52ce5a0cf..b411628e7f9d9884336cb61ab24cf450d97e094a 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -208,7 +208,7 @@ Section list_theory.
 
     Lemma list_agrees_fmap `{Equivalence _ R'} al :
       list_agrees R al → list_agrees R' (f <$> al).
-    Proof using All.
+    Proof using Type*.
       move=> /list_agrees_alt Hl. apply (list_agrees_alt R') => a' b'.
       intros (a & -> & Ha)%elem_of_list_fmap (b & -> & Hb)%elem_of_list_fmap.
       apply Hf. exact: Hl.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 42cfa073ac41bdaa4ef6ef2d1894ffafdb9feaab..25b17ea48256aa2376433d2bd55d3349c6af07de 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export excl local_updates.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import classes.
-Set Default Proof Using "Type*".
+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 77fdad01703247c6cfba8e12041aded5c56fa891..fe4af017e2c0b23d312203def85fe9bbd8bded9f 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,6 +1,6 @@
 From mathcomp Require Export ssreflect.
 From iris.prelude Require Export prelude.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.
 Ltac done := prelude.tactics.done.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index c4205ca16adb76ebea6cb29b95177f7be4c71816..138f7a2e8cb2aa257c028543f02be39f0bf08db0 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Class PCore (A : Type) := pcore : A → option A.
 Instance: Params (@pcore) 2.
@@ -428,6 +428,7 @@ Qed.
 
 (** ** Total core *)
 Section total_core.
+  Set Default Proof Using "Type*".
   Context `{CMRATotal A}.
 
   Lemma cmra_core_l x : core x ⋅ x ≡ x.
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index 12448601ea5f605cdb272e963b81ea8b6f9a1966..09082283a63fb654c9de0ed606673a9bde059b4d 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra list.
 From iris.prelude Require Import functions gmap gmultiset.
-Set Default Proof Using "Type*".
+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 08645cf328b169c68f55b4ba751686df22c3d173..445aee068e3b794a57ce1fe5500bd224c9adf0ca 100644
--- a/theories/algebra/cmra_tactics.v
+++ b/theories/algebra/cmra_tactics.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import cmra_big_op.
-Set Default Proof Using "Type*".
+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 0f48c62fd9a20f264e114d2b2e5c34b93c2b9e38..605adfde185d8d2beaa4fd9eefbb4443f0bf7986 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections coPset.
-Set Default Proof Using "Type*".
+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 bb2396e0e9394b5d55a2676cc9614edbbcd54ae3..d7823128b15669c07a73bc2120f5eb256906e9d2 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -205,7 +205,7 @@ Instance fold_ne : Proper (dist n ==> dist n) fold.
 Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
-Proof using All.
+Proof using Type*.
   apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
   - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
     rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index b8d3bb35970b9f7d834fccfd98bf36c4999981a1..05bdbd34029621f632f2ffd9b2583101fbe3e188 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import local_updates.
-Set Default Proof Using "Type*".
+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 0d3c5b62adbef48a5ebde5327428df792a310700..3ff595195b3de5228a84d27217d1ae5ea511d319 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import ofe cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* Old notation for backwards compatibility. *)
 
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index d79ad7928c3515c5a3762e19a9cc165183e8c913..496775226fbb9819c81a82b9a3a9c38bc897bf3e 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra updates.
-Set Default Proof Using "Type*".
+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 ecb517229f4ef1db68fa92201b637deab6aa5182..d1ebb4648a4e3c75786edbc7d369902a853a3dd2 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index ee5cd143e9cec6ee5184fa4c5c5d73241ae56ab5..6ba732e05c632e146b6ba82015b636f3831424bb 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -1,6 +1,6 @@
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Notation frac := Qp (only parsing).
 
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index c2272a18c9048014ffaca1042b7fe48cb859a1ed..b3f13832ca080613c070fa84bf86a3b16d8b3550 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -2,7 +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*".
+Set Default Proof Using "Type".
 
 Section cofe.
 Context `{Countable K} {A : ofeT}.
@@ -334,6 +334,7 @@ Proof.
 Qed.
 
 Section freshness.
+  Set Default Proof Using "Type*".
   Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
     ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index a0a97f6f1286ec7d748a12bb17713993f87eb6c3..94b39dbdc51306f5e9717bd10d58c2b5cdbb2b99 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Export collections gmap mapset.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (* The union CMRA *)
 Section gset.
@@ -155,6 +155,7 @@ Section gset_disj.
   Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
 
   Section fresh_updates.
+    Set Default Proof Using "Type*".
     Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 
     Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index 479e74c2f0a9a610ab71555b15c0ddf542117058..581c7207f4444a1ce0233b3a66fb2a734f35e971 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
 From iris.prelude Require Import finite.
-Set Default Proof Using "Type*".
+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 61f773f0bd1ac20e6ec8c6e37854f5e0c25516c9..e2049d9bf98000326c8d32404010facbf05e384e 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -2,7 +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*".
+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 9f6dde631dc38a7854a7a609796d2160bbb3d3d0..e465e9e686344697260b51c6586483448e95ffd1 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+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 d2dc52b798bf5d1b4c5cf1de55c3057da6dd0336..b7c6ec82d0f62a2ddbf10c28a2c08dd3cef45acc 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export base.
-Set Default Proof Using "Type*".
+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
@@ -159,6 +159,7 @@ Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
 Proof. by intros n y1 y2. Qed.
 
 Section contractive.
+  Set Default Proof Using "Type*".
   Context {A B : ofeT} (f : A → B) `{!Contractive f}.
   Implicit Types x y : A.
 
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index b52eca914f52c8557b4cb034513315b4dd50cf41..632313e618c9dfb6cae54d1b17ed27b44a282464 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -1,7 +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*".
+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 35d63746e13d986dec87fe5cc27a3016f50d95c2..ac2d3a54dcc13aacf33250b066249401796a45ef 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** * Frame preserving updates *)
 (* This quantifies over [option A] for the frame.  That is necessary to
@@ -86,6 +86,7 @@ Qed.
 
 (** ** Frame preserving updates for total CMRAs *)
 Section total_updates.
+  Set Default Proof Using "Type*".
   Context `{CMRATotal A}.
 
   Lemma cmra_total_updateP x (P : A → Prop) :
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index c390c1a19389b20250b82b756de3ae4b540e28af..e0094eed172d4fa9e9d74e35a0273d6943d5b57b 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -1,7 +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*".
+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 0d84d12c3ce3804f4b8a548ddc4c442dd5216e0f..701ff8357f9f8c43d9e446f76024b94a6c0fc15f 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export derived.
-Set Default Proof Using "Type*".
+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 2a995bab1a38062d9d2a05545aeabed7e5c7329d..8eb08543ebc320f2af23e990b765adf271844172 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Export list cmra_big_op.
 From iris.base_logic Require Export base_logic.
 From iris.prelude Require Import gmap fin_collections gmultiset functions.
-Set Default Proof Using "Type*".
+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 e873c05341c7527274cdbdef7cb24f788c2ed8c1..4d4995e42430015c9aef59d887d5b85cd64d472f 100644
--- a/theories/base_logic/deprecated.v
+++ b/theories/base_logic/deprecated.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import primitive.
-Set Default Proof Using "Type*".
+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 16746c06a5f5673cc9287d22b0756f97b3db4741..b15ba0355e35f7999af0f38c93ff77809c049989 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export primitive.
-Set Default Proof Using "Type*".
+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 95598242b5b314ca796fe94da904cad9898db1bc..fb692ba9a260e11e9e3fc825d420d9fb2d5b07a9 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Import base_logic.
-Set Default Proof Using "Type*".
+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 *)
@@ -274,7 +274,7 @@ Qed.
 Section classical.
 Context (not_all_not_ex: ∀ (P : M → Prop), ¬ (∀ n : M, ¬ P n) → ∃ n : M, P n).
 Lemma nnupd_bupd P:  (|=n=> P) ⊢ (|==> P).
-Proof.
+Proof using Type*.
   rewrite /uPred_nnupd.
   split. uPred.unseal; red; rewrite //=.
   intros n x ? Hforall k yf Hle ?.
diff --git a/theories/base_logic/hlist.v b/theories/base_logic/hlist.v
index 26a01fa5e7f3b42e23301f93b6f0c134ce75c4b2..5196fe0f9c384608a030ef607e8797079836f33b 100644
--- a/theories/base_logic/hlist.v
+++ b/theories/base_logic/hlist.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Export hlist.
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type*".
+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 8f1f42242242b35b3ba194dde20cfd3eecc02df2..7225f2d1f628179c9c2611b01c7f3fc57ccdbb21 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -3,7 +3,7 @@ From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 (* The CMRA we need. *)
@@ -117,7 +117,7 @@ Section auth.
     ▷ auth_inv γ f φ ∗ auth_own γ a ={E}=∗ ∃ t,
       ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
       ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E}=∗ ▷ auth_inv γ f φ ∗ auth_own γ b.
-  Proof.
+  Proof using Type*.
     iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
     iDestruct "Hinv" as (t) "[>Hγa Hφ]".
     iModIntro. iExists t.
@@ -133,7 +133,7 @@ Section auth.
     auth_ctx γ N f φ ∗ auth_own γ a ={E,E∖↑N}=∗ ∃ t,
       ⌜a ≼ f t⌝ ∗ ▷ φ t ∗ ∀ u b,
       ⌜(f t, a) ~l~> (f u, b)⌝ ∗ ▷ φ u ={E∖↑N,E}=∗ auth_own γ b.
-  Proof.
+  Proof using Type*.
     iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
        [auth_acc] and [inv_open] -- but since we don't have any good support
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 4e76e7d12692879cde13cbf931061eba195d3d35..d5e0b98fc91040126a56e3f80163897f955604dc 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import auth gmap agree.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+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 c7f55710e9d8ef9d5ce0ad6c680bcb76f79e1868..c06067a316eff18ce774362c4f62191b46fba593 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants fractional.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+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 1bef3566af60bbe861c9ed69a4212b7b017be5a6..6630d803a2bc315e3fd795277883eda227559417 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+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 f325fc8e60e38b16f2d5b1e07f62499524d1f395..d9f02cf5bec7003bbec19138ab250dc564968cdc 100644
--- a/theories/base_logic/lib/counter_examples.v
+++ b/theories/base_logic/lib/counter_examples.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import base_logic soundness.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "All".
+Set Default Proof Using "Type*".
 
 (** This proves that we need the â–· in a "Saved Proposition" construction with
 name-dependent allocation. *)
@@ -39,7 +39,7 @@ Module savedprop. Section savedprop.
   Qed.
 
   Lemma contradiction : False.
-  Proof.
+  Proof using All.
     apply (@soundness M False 1); simpl.
     iIntros "". iMod A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
@@ -186,7 +186,7 @@ Module inv. Section inv.
   Qed.
 
   Lemma contradiction : False.
-  Proof.
+  Proof using All.
     apply consistency. iIntros "".
     iMod A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index c5d70fb1758d2c035341915f6e62d00922297022..6485be49e97315b6448239ca7e849f13ab56481c 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
-Set Default Proof Using "Type*".
+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 3f39eda433fc4c0d6117b0714b18561b0034a4d5..af12736d1da3f2cab1b19a2557315d136c84f358 100644
--- a/theories/base_logic/lib/fractional.v
+++ b/theories/base_logic/lib/fractional.v
@@ -2,7 +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*".
+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 7579343d671ceef7e9345240c3bc67dcb3c57fc6..8711a209d5f14875478250d5bdf45a0cbffb5c3b 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import auth gmap frac agree.
 From iris.base_logic.lib Require Export own.
 From iris.base_logic.lib Require Import fractional.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+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 3ecab752949142fa39fa6ec08473046bf732ce85..5d002b353e4726d01a61bcbeffdcd9e40b9b37ad 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates namespaces.
 From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
-Set Default Proof Using "Type*".
+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 730e8b518d0f92f350ea7ca94cbec5c25c9ad2c0..95a378c30aa8827ddcf550230875418735cb816d 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import iprod gmap.
 From iris.algebra Require cofe_solver.
-Set Default Proof Using "Type*".
+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 9a72acc20579772f05288f7bb3aedfd1f5fa8077..5837dcb68ad17aa6fc6daa69f6e9238411e3581e 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+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 970b1ee9e3430e4179d62a0c1fa6d25b192df510..f9610bb371087348ccbce885eb82b22e882d0459 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
-Set Default Proof Using "Type*".
+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 f1f3c4d0cafba2c36e14cb5729a0da78037f37be..1390c6a583b925e5b7782e610fdf5404ac4e752a 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import iprod gmap.
 From iris.base_logic Require Import big_op.
 From iris.base_logic Require Export iprop.
 From iris.proofmode Require Import classes.
-Set Default Proof Using "Type*".
+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 e0c8f2150dfd759aada97ff4a00dfc920a29aa6e..7fc022f00844cd212375214e2b10d88a8ae20949 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
 From iris.prelude Require Import gmap.
-Set Default Proof Using "Type*".
+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 8776ec6c4b9588e205522c6227616af9a3f9bcf3..6aae15aa62568343834aa905e54bf42f8bebe9d8 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+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 aecea9568b29c9d04ac275491441a952a4a86795..906965920c1c12652cfea4b8ced04247db6564a6 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
+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 7a047ab41c04e2d03b3455b25f39a20142622052..850b62678fb62e03e1b52359576ea7dd3b9f8758 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -3,7 +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*".
+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 db9f2b6b759db223a8d88f48cecc17d34a01f837..0ad4f620874b077c0a7c18fbb94bf1640d08bcee 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Export upred.
 From iris.algebra Require Export updates.
-Set Default Proof Using "Type*".
+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 a9f04c1e1a4f9ae68e6f4814d839f4475e264e91..105cb7503ed0ae3387c4ee7f8ae8148d5d02df01 100644
--- a/theories/base_logic/soundness.v
+++ b/theories/base_logic/soundness.v
@@ -1,5 +1,5 @@
 From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Section adequacy.
diff --git a/theories/base_logic/tactics.v b/theories/base_logic/tactics.v
index 040d0ce7793675c88355ddd7e0655b2dc71c8d9b..91e286dc475a2db57b31db5de1556eb31ae8e24a 100644
--- a/theories/base_logic/tactics.v
+++ b/theories/base_logic/tactics.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Import gmap.
 From iris.base_logic Require Export base_logic big_op.
-Set Default Proof Using "Type*".
+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 c10ca59676419a91ec1d9f5ce99ed1bfe7fd6b05..0ac232c72952ca916afb8f7c528a2d0d75b2bc15 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 (** The basic definition of the uPred type, its metric and functor laws.
     You probably do not want to import this file. Instead, import