diff --git a/iris b/iris
index 5e3835f807768f42f77b6cc33bca039b8274a586..8f33e2828ae7b286adee0071ffa5c40fb4977fcd 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 5e3835f807768f42f77b6cc33bca039b8274a586
+Subproject commit 8f33e2828ae7b286adee0071ffa5c40fb4977fcd
diff --git a/theories/lifetime.v b/theories/lifetime.v
index 4d705fdb6e1d6047c6a8ab98bd7b586f4297608d..193be22d9c33f4cd72d93a75ae95384bdc37bc1c 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -3,7 +3,6 @@ From iris.base_logic.lib Require Export fancy_updates invariants namespaces.
 From iris.proofmode Require Import tactics.
 
 Definition lftN := nroot .@ "lft".
-
 Definition atomic_lft := positive.
 
 Definition lft_tokUR : ucmraT :=
@@ -185,7 +184,7 @@ Section lft.
   Lemma lft_own_static q : True ==∗ q.[static].
   Proof.
     rewrite /lft_own /static omap_empty fmap_empty.
-    apply (own_empty (A:=lft_tokUR) lft_toks_name).
+    apply (own_empty lft_tokUR lft_toks_name).
   Qed.
 
   Lemma lft_not_dead_static : [† static] ⊢ False.
diff --git a/theories/perm.v b/theories/perm.v
index ff98376657d96071113652d77c54761442422360..fbe763f4eddc1fbc07f8b492dcce6365ae5c91e6 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -91,7 +91,6 @@ Section duplicable.
 
 End duplicable.
 
-Hint Extern 0 (Is_true _.(ty_dup)) => exact I.
 
 Section has_type.
 
diff --git a/theories/type.v b/theories/type.v
index 348046e5ba3d7e184829a226537b97963c0f51cd..ebc124bc32a755adcd645aa66ae94439131b6e1d 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -22,7 +22,8 @@ Section type.
 Context `{iris_typeG Σ}.
 
 Record type :=
-  { ty_size : nat; ty_dup : bool;
+  { ty_size : nat;
+    ty_dup : bool;
     ty_own : thread_id → list val → iProp Σ;
     ty_shr : lifetime → thread_id → coPset → loc → iProp Σ;
 
@@ -108,6 +109,9 @@ Qed.
 
 End type.
 
+Hint Extern 0 (Is_true _.(ty_dup)) =>
+  exact I || assumption : typeclass_instances.
+
 Delimit Scope lrust_type_scope with T.
 Bind Scope lrust_type_scope with type.
 
@@ -317,8 +321,8 @@ Section types.
     repeat setoid_rewrite tl_own_union; first last.
     set_solver. set_solver. set_solver. set_solver.
     iDestruct "Htl" as "[[Htl1 Htl2] $]".
-    iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". set_solver.
-    iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". set_solver.
+    iMod (ty1.(ty_shr_acc) with "LFT H1 [$Htok1 $Htl1]") as (q1) "[H1 Hclose1]". done. set_solver.
+    iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". done. set_solver.
     destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
     iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
     rewrite -!heap_mapsto_vec_op_eq !split_prod_mt.