diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 9951b8e479db26a6012ca72b11047c19a2beffba..fd31d79ba9424acc4e9cdf23d0c7f2a4263f8835 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -3,7 +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*".
+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 76b2b167bf94b3decd6c6330b0fc94a0649787af..646ebbdcae4658fce73c6687eeeab2ec76b10241 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -2,7 +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*".
+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 df02d3969ee7e6a885cdc7ae7aa87d9e12d25675..e0c0f468b7a493ae7de2a48c196d64249de57361 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -1,12 +1,11 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
 From iris.proofmode Require Import tactics.
-(* FIXME: This file needs a 'Proof Using' hint, but the default we use
-   everywhere makes for lots of extra ssumptions. *)
+Set Default Proof Using "Type".
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ} `{Inhabited state}.
+Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types v : val.
@@ -37,7 +36,7 @@ Lemma wp_lift_pure_head_step E Φ e1 :
   (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
     WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof.
+Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
   iIntros (????). iApply "H". eauto.
 Qed.
@@ -77,7 +76,7 @@ Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
-Proof. eauto using wp_lift_pure_det_step. Qed.
+Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
 Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   to_val e1 = None →
@@ -85,7 +84,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-Proof.
+Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
 Qed.
 End wp.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 74da06afcedc81a80c5ed3c41527529cd02bc2fb..ee98518676af7ea9a0793f00f21d1244f8c43bab 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -2,7 +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*".
+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 b5ca5a347f18a71591028738222c39f3d7bcb2d3..0cb4f409cc827151b3bd8d309a04bc1efb50bafc 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -1,7 +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*".
+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 3227a06e1aa6f50b79740fa88c9ac318788f7cb8..21fc2e3a1428bd494a955b691a4ad77426a111c1 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export ofe.
-Set Default Proof Using "Type*".
+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 b56edc5568a781bd99d14bc90cd987fdf000205f..82706be47ebb3ee96e5622835ccd789398a9297e 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -1,7 +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*".
+Set Default Proof Using "Type".
 
 Section lifting.
 Context `{irisG Λ Σ}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index e57910e9fdd8f1e26e5b8949d6ee1470ac2cb0e7..0a98629860f2a6e045883bb5f8e6d0c031e1402d 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -3,7 +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*".
+Set Default Proof Using "Type".
 
 Class ownPG' (Λstate : Type) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
@@ -158,7 +158,7 @@ End lifting.
 Section ectx_lifting.
   Import ectx_language.
   Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-  Context `{ownPG (ectx_lang expr) Σ} `{Inhabited state}.
+  Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
   Implicit Types Φ : val → iProp Σ.
   Implicit Types e : expr.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
@@ -181,7 +181,7 @@ Section ectx_lifting.
     (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
       WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
     ⊢ WP e1 @ E {{ Φ }}.
-  Proof.
+  Proof using Hinh.
     iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
     iIntros (????). iApply "H". eauto.
   Qed.
@@ -220,14 +220,14 @@ Section ectx_lifting.
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
     ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
     ⊢ WP e1 @ E {{ Φ }}.
-  Proof. eauto using wp_lift_pure_det_step. Qed.
+  Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
   Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-  Proof.
+  Proof using Hinh.
     intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index b75cb874b2c6be8efd1ac143caeda06e2d95ebdc..98a08018f3f570b438a5939c778eba998260d9c3 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -2,7 +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*".
+Set Default Proof Using "Type".
 Import uPred.
 
 Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {