Fix compilation with current Iris.

iris @ 8f33e282

-Subproject commit 5e3835f807768f42f77b6cc33bca039b8274a586
+Subproject commit 8f33e2828ae7b286adee0071ffa5c40fb4977fcd

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.

theories/perm.v

@@ -91,7 +91,6 @@ Section duplicable.
 
 End duplicable.
 
-Hint Extern 0 (Is_true _.(ty_dup)) => exact I.
 
 Section has_type.
 

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.