From 60d82286172f9b82c9b8b8cecc267da91fac6ab1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Jan 2017 19:10:04 +0100
Subject: [PATCH] more restrictive Proof Using hints in heap_lang, proofmode,
 tests

---
 theories/heap_lang/adequacy.v                  | 2 +-
 theories/heap_lang/lang.v                      | 2 +-
 theories/heap_lang/lib/assert.v                | 2 +-
 theories/heap_lang/lib/barrier/barrier.v       | 2 +-
 theories/heap_lang/lib/barrier/proof.v         | 2 +-
 theories/heap_lang/lib/barrier/protocol.v      | 2 +-
 theories/heap_lang/lib/barrier/specification.v | 5 +++--
 theories/heap_lang/lib/counter.v               | 2 +-
 theories/heap_lang/lib/lock.v                  | 2 +-
 theories/heap_lang/lib/par.v                   | 3 ++-
 theories/heap_lang/lib/spawn.v                 | 2 +-
 theories/heap_lang/lib/spin_lock.v             | 2 +-
 theories/heap_lang/lib/ticket_lock.v           | 2 +-
 theories/heap_lang/lifting.v                   | 2 +-
 theories/heap_lang/notation.v                  | 2 +-
 theories/heap_lang/proofmode.v                 | 2 +-
 theories/heap_lang/tactics.v                   | 2 +-
 theories/proofmode/class_instances.v           | 2 +-
 theories/proofmode/classes.v                   | 2 +-
 theories/proofmode/coq_tactics.v               | 2 +-
 theories/proofmode/environments.v              | 2 +-
 theories/proofmode/intro_patterns.v            | 2 +-
 theories/proofmode/notation.v                  | 2 +-
 theories/proofmode/sel_patterns.v              | 2 +-
 theories/proofmode/spec_patterns.v             | 2 +-
 theories/proofmode/strings.v                   | 2 +-
 theories/proofmode/tactics.v                   | 2 +-
 theories/tests/barrier_client.v                | 5 +++--
 theories/tests/counter.v                       | 2 +-
 theories/tests/heap_lang.v                     | 2 +-
 theories/tests/joining_existentials.v          | 5 +++--
 theories/tests/list_reverse.v                  | 2 +-
 theories/tests/one_shot.v                      | 3 ++-
 theories/tests/proofmode.v                     | 2 +-
 theories/tests/tree_sum.v                      | 2 +-
 35 files changed, 43 insertions(+), 38 deletions(-)

diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index c1d938a6..3d5ba129 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -3,7 +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*".
+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 6a8cc104..936039b3 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -2,7 +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*".
+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 3569ae28..93742d45 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -2,7 +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*".
+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 311ec503..7ae83e5d 100644
--- a/theories/heap_lang/lib/barrier/barrier.v
+++ b/theories/heap_lang/lib/barrier/barrier.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export notation.
-Set Default Proof Using "Type*".
+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 dd392818..7f691d03 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -5,7 +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*".
+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 c49a260d..f9f57224 100644
--- a/theories/heap_lang/lib/barrier/protocol.v
+++ b/theories/heap_lang/lib/barrier/protocol.v
@@ -1,7 +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*".
+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 7af0c8f2..e69e81a5 100644
--- a/theories/heap_lang/lib/barrier/specification.v
+++ b/theories/heap_lang/lib/barrier/specification.v
@@ -2,11 +2,12 @@ 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*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Section spec.
-Context `{!heapG Σ} `{!barrierG Σ}.
+Set Default Proof Using "Type*".
+Context `{!heapG Σ, !barrierG Σ}.
 
 Lemma barrier_spec (N : namespace) :
   ∃ recv send : loc → iProp Σ -n> iProp Σ,
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 2923d524..8d13ca82 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -4,7 +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*".
+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 9780eef8..dcae7f0a 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export lifting notation.
 From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type*".
+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 57130804..95bc308b 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Export spawn.
 From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Definition parN : namespace := nroot .@ "par".
@@ -14,6 +14,7 @@ Definition par : val :=
 Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
 
 Section proof.
+Set Default Proof Using "Type*".
 Context `{!heapG Σ, !spawnG Σ}.
 
 (* Notice that this allows us to strip a later *after* the two Ψ have been
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 52cd71b2..d8e6e6bf 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -4,7 +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*".
+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 9349d0c1..18c37ea8 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -4,7 +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*".
+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 2b688992..8bfe6f6d 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -4,7 +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*".
+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 e7fe25de..660163a7 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -5,7 +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*".
+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 d36311ea..d2ee452b 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang tactics.
-Set Default Proof Using "Type*".
+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 38eb5ed8..00724254 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -2,7 +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*".
+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 11ae6e41..9d3cd281 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Export lang.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 Import heap_lang.
 
 (** We define an alternative representation of expressions in which the
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index d246dd8a..b7477648 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -2,7 +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*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Section classes.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 26cdd99a..8e66e899 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.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 classes.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index b252263d..394c5d7c 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -2,7 +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*".
+Set Default Proof Using "Type".
 Import uPred.
 Import env_notations.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 37138104..3b2df1ec 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -2,7 +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*".
+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 a15af76e..3f7f1b5e 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+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 d563702f..57b08033 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics environments.
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+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 9bc9c8ca..d520504b 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+Set Default Proof Using "Type".
 
 Inductive sel_pat :=
   | SelPure
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 92bd0c6b..8c1d836d 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,5 +1,5 @@
 From iris.prelude Require Export strings.
-Set Default Proof Using "Type*".
+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 3ed00474..b3d547d0 100644
--- a/theories/proofmode/strings.v
+++ b/theories/proofmode/strings.v
@@ -1,7 +1,7 @@
 From iris.prelude Require Import strings.
 From iris.algebra Require Import base.
 From Coq Require Import Ascii.
-Set Default Proof Using "Type*".
+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 e535ccaa..a3234559 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -5,7 +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*".
+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 9490c527..9a91478f 100644
--- a/theories/tests/barrier_client.v
+++ b/theories/tests/barrier_client.v
@@ -3,7 +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*".
+Set Default Proof Using "Type".
 
 Definition worker (n : Z) : val :=
   λ: "b" "y", wait "b" ;; !"y" #n.
@@ -14,9 +14,10 @@ Definition client : expr :=
     (worker 12 "b" "y" ||| worker 17 "b" "y").
 
 Section client.
+  Set Default Proof Using "Type*".
   Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
 
-  Local Definition N := nroot .@ "barrier".
+  Definition N := nroot .@ "barrier".
 
   Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
     (∃ f : val, l ↦{q} f ∗ □ ∀ n : Z, WP f #n {{ v, ⌜v = #(n + 42)⌝ }})%I.
diff --git a/theories/tests/counter.v b/theories/tests/counter.v
index baa9d394..e8ced803 100644
--- a/theories/tests/counter.v
+++ b/theories/tests/counter.v
@@ -8,7 +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*".
+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 733b38f2..478e09a0 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -3,7 +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*".
+Set Default Proof Using "Type".
 
 Section LiftingTests.
   Context `{heapG Σ}.
diff --git a/theories/tests/joining_existentials.v b/theories/tests/joining_existentials.v
index cbf39efb..2f5ce6df 100644
--- a/theories/tests/joining_existentials.v
+++ b/theories/tests/joining_existentials.v
@@ -4,7 +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".
+Set Default Proof Using "Type".
 
 Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
   csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
@@ -24,6 +24,7 @@ Definition client eM eW1 eW2 : expr :=
   (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
 
 Section proof.
+Set Default Proof Using "Type*".
 Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
 Context (N : namespace).
 Local Notation X := (F (iProp Σ)).
@@ -71,7 +72,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
   (∀ x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -∗
   (∀ x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -∗
   WP client eM eW1 eW2 {{ _, ∃ γ, barrier_res γ Ψ }}.
-Proof.
+Proof using All.
   iIntros "/= HP #He #He1 #He2"; rewrite /client.
   iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
   wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
diff --git a/theories/tests/list_reverse.v b/theories/tests/list_reverse.v
index 0a9943a5..cdee4262 100644
--- a/theories/tests/list_reverse.v
+++ b/theories/tests/list_reverse.v
@@ -3,7 +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*".
+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 d657830c..bd5adb85 100644
--- a/theories/tests/one_shot.v
+++ b/theories/tests/one_shot.v
@@ -3,7 +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*".
+Set Default Proof Using "Type".
 
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
@@ -30,6 +30,7 @@ Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
+Set Default Proof Using "Type*".
 Context `{!heapG Σ, !one_shotG Σ}.
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 8f847968..147edd8e 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
-Set Default Proof Using "Type*".
+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 09d31781..dfcb13d2 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -2,7 +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*".
+Set Default Proof Using "Type".
 
 Inductive tree :=
   | leaf : Z → tree
-- 
GitLab