diff --git a/opam b/opam
index 224547ed553fec48c2bf6d997636c48506479993..a958ad4a29e3787d4d66592c759577b7f17e3cea 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-iris" { (= "dev.2019-08-29.2.b75bb397") | (= "dev") }
+  "coq-iris" { (= "dev.2019-09-13.1.708b8ac0") | (= "dev") }
 ]
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 4bac769097151f753dddbf74c9c84638fac99ab6..2daa85ad6d02cb4ebf39bfa67e6ba347a0b7c1b3 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,8 +1,8 @@
+From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting.
 From lrust.lang Require Export lang heap.
 From lrust.lang Require Import tactics.
-From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 223518ceeb5c25ddc15c2f81fd9625ee8fe2f3ca..ef5c8bd70b9cefd5f0f86c94a7dec39ecbc795c2 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,8 +1,8 @@
-From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
-From lrust.lang Require Export tactics lifting.
+From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting.
+From lrust.lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/typing/base.v b/theories/typing/base.v
index c04533a9fcef852bc292e9b74e1e0c7d3a05c298..f5a8b0029464777523b6172e554b656138633dbb 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,6 +1,12 @@
 From lrust.lang Require Export proofmode.
 From lrust.lifetime Require Export frac_borrow.
 
+(* Last, so that we make sure we shadow the defintion of delete for
+   sets coming from the prelude. *)
+From lrust.lang.lib Require Export new_delete.
+
+Open Scope Z_scope.
+
 Create HintDb lrust_typing.
 Create HintDb lrust_typing_merge.
 
@@ -28,4 +34,4 @@ Hint Resolve <- elem_of_app : lrust_typing.
 (* done is there to handle equalities with constants *)
 Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
 Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
-Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
\ No newline at end of file
+Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index f1df0427576a2c3ae7254b18e29f2f4282c58752..c92f87bd17368db5ee5a3de11a3a9e4cf3124af8 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -21,7 +21,7 @@ Section join.
                             letcall: "r" := "call_once_A" ["fA"]%E in
                             finish ["c"; "r"]] in
       letcall: "retB" := "call_once_B" ["fB"]%E in
-      let: "retA" := join ["join"] in
+      let: "retA" := spawn.join ["join"] in
       (* Put the results in a pair. *)
       let: "ret" := new [ #(R_A.(ty_size) + R_B.(ty_size)) ] in
       "ret" +ₗ #0 <-{R_A.(ty_size)} !"retA";;
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 3512082bfa86fd0eb981348c2d50d412e7e7034d..53a3a252cd97e388f9c503ceef12f72b0aaef129 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -110,7 +110,7 @@ Section spawn.
   Definition join : val :=
     funrec: <> ["c"] :=
       let: "c'" := !"c" in
-      let: "r" := join ["c'"] in
+      let: "r" := spawn.join ["c'"] in
       delete [ #1; "c"];; return: ["r"].
 
   Lemma join_type retty `{!TyWf retty} :
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index 2b631d86e26b58ef14952deccbfda3bd703e3ac1..860b1c07be5d4633d843b8b5ed85b843e1b3eaf1 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
-From lrust.typing Require Import typing.
 From lrust.lang.lib Require Import swap.
+From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
 Section swap.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 7280e94c066d27dce09f30ca1eca130d0958e0bd..f55191b3948ce30ec0d6af50b2a57bd65ee09efa 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,6 +1,6 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
-From lrust.lang.lib Require Import new_delete memcpy.
+From lrust.lang.lib Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
@@ -254,7 +254,7 @@ Section typing.
     iApply wp_new; try done. iModIntro.
     iIntros (l) "(H† & Hlft)". rewrite tctx_interp_singleton tctx_hasty_val.
     iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
-    iExists (repeat #☠ (Z.to_nat n)). iFrame. by rewrite /= repeat_length. 
+    iExists (repeat #☠ (Z.to_nat n)). iFrame. by rewrite /= repeat_length.
   Qed.
 
   Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 5b61f4b51d7c009e2f9915b01871d9645f76a8b0..bee83efcf7428635d86876c6ec89df5695bb4e05 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,7 +3,3 @@ From lrust.typing Require Export
   lft_contexts type_context cont_context programs cont type
   int bool own uniq_bor shr_bor uninit product sum fixpoint function
   product_split borrow type_sum.
-
-(* Last, so that we make sure we shadow the defintion of delete for
-   sets coming from the prelude. *)
-From lrust.lang Require Export new_delete.