From d6b49ab29e15031e47cb1644166172db52aea5ca Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Jan 2017 19:24:36 +0100
Subject: [PATCH] more restrictive Proof Using hints in base_logic, algebra

---
 theories/algebra/agree.v                        | 2 +-
 theories/algebra/auth.v                         | 2 +-
 theories/algebra/base.v                         | 2 +-
 theories/algebra/cmra.v                         | 3 ++-
 theories/algebra/cmra_big_op.v                  | 2 +-
 theories/algebra/cmra_tactics.v                 | 2 +-
 theories/algebra/coPset.v                       | 2 +-
 theories/algebra/cofe_solver.v                  | 2 +-
 theories/algebra/csum.v                         | 2 +-
 theories/algebra/deprecated.v                   | 2 +-
 theories/algebra/dra.v                          | 2 +-
 theories/algebra/excl.v                         | 2 +-
 theories/algebra/frac.v                         | 2 +-
 theories/algebra/gmap.v                         | 3 ++-
 theories/algebra/gset.v                         | 3 ++-
 theories/algebra/iprod.v                        | 2 +-
 theories/algebra/list.v                         | 2 +-
 theories/algebra/local_updates.v                | 2 +-
 theories/algebra/ofe.v                          | 3 ++-
 theories/algebra/sts.v                          | 2 +-
 theories/algebra/updates.v                      | 3 ++-
 theories/algebra/vector.v                       | 2 +-
 theories/base_logic/base_logic.v                | 2 +-
 theories/base_logic/big_op.v                    | 2 +-
 theories/base_logic/deprecated.v                | 2 +-
 theories/base_logic/derived.v                   | 2 +-
 theories/base_logic/double_negation.v           | 4 ++--
 theories/base_logic/hlist.v                     | 2 +-
 theories/base_logic/lib/auth.v                  | 6 +++---
 theories/base_logic/lib/boxes.v                 | 2 +-
 theories/base_logic/lib/cancelable_invariants.v | 2 +-
 theories/base_logic/lib/core.v                  | 2 +-
 theories/base_logic/lib/counter_examples.v      | 6 +++---
 theories/base_logic/lib/fancy_updates.v         | 2 +-
 theories/base_logic/lib/fractional.v            | 2 +-
 theories/base_logic/lib/gen_heap.v              | 2 +-
 theories/base_logic/lib/invariants.v            | 2 +-
 theories/base_logic/lib/iprop.v                 | 2 +-
 theories/base_logic/lib/na_invariants.v         | 2 +-
 theories/base_logic/lib/namespaces.v            | 2 +-
 theories/base_logic/lib/own.v                   | 2 +-
 theories/base_logic/lib/saved_prop.v            | 2 +-
 theories/base_logic/lib/sts.v                   | 2 +-
 theories/base_logic/lib/viewshifts.v            | 2 +-
 theories/base_logic/lib/wsat.v                  | 2 +-
 theories/base_logic/primitive.v                 | 2 +-
 theories/base_logic/soundness.v                 | 2 +-
 theories/base_logic/tactics.v                   | 2 +-
 theories/base_logic/upred.v                     | 2 +-
 49 files changed, 59 insertions(+), 54 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 11cf3fb30..b411628e7 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 42cfa073a..25b17ea48 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 77fdad017..fe4af017e 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 c4205ca16..138f7a2e8 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 12448601e..09082283a 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 08645cf32..445aee068 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 0f48c62fd..605adfde1 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 bb2396e0e..d7823128b 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 b8d3bb359..05bdbd340 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 0d3c5b62a..3ff595195 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 d79ad7928..496775226 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 ecb517229..d1ebb4648 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 ee5cd143e..6ba732e05 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 c2272a18c..b3f13832c 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 a0a97f6f1..94b39dbdc 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 479e74c2f..581c7207f 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 61f773f0b..e2049d9bf 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 9f6dde631..e465e9e68 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 d2dc52b79..b7c6ec82d 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 b52eca914..632313e61 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 35d63746e..ac2d3a54d 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 c390c1a19..e0094eed1 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 0d84d12c3..701ff8357 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 2a995bab1..8eb08543e 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 e873c0534..4d4995e42 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 16746c06a..b15ba0355 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 95598242b..fb692ba9a 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 26a01fa5e..5196fe0f9 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 8f1f42242..7225f2d1f 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 4e76e7d12..d5e0b98fc 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 c7f55710e..c06067a31 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 1bef3566a..6630d803a 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 f325fc8e6..d9f02cf5b 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 c5d70fb17..6485be49e 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 3f39eda43..af12736d1 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 7579343d6..8711a209d 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 3ecab7529..5d002b353 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 730e8b518..95a378c30 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 9a72acc20..5837dcb68 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 970b1ee9e..f9610bb37 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 f1f3c4d0c..1390c6a58 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 e0c8f2150..7fc022f00 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 8776ec6c4..6aae15aa6 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 aecea9568..906965920 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 7a047ab41..850b62678 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 db9f2b6b7..0ad4f6208 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 a9f04c1e1..105cb7503 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 040d0ce77..91e286dc4 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 c10ca5967..0ac232c72 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
-- 
GitLab