diff --git a/theories/typing/base.v b/theories/typing/base.v
index 64cb2927efd91369b80302f8a695e2aafcb10fa0..796d22432f973267b4883b6c22e4bcb0df81df20 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -1,6 +1,12 @@
 From lrust.lifetime Require Export frac_borrow.
 From gpfsl.base_logic Require Import na.
 
+(* Last, so that we make sure we shadow the definition 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.
 
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 3c01169109431d54448e19528c00fa2ad2b84afc..c6a3fd721cc6b77bf4aa5b796496fc11d8316a8c 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 4ca1c03d6a1eec310ae7a201d84217a47cfc8da0..772d602e255c05626f1f65088d87c64084873257 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -113,7 +113,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 161efa5ef83715e617f33d0469aadd91dd2b6e24..d5fc5b1557cb9906e95cb5ad7b16ef016ccab850 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -1,5 +1,5 @@
-From lrust.typing Require Import typing.
 From lrust.lang 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 d73f29500b7da92a4f8d0fc2c995d020e9e15455..3bed184b91ecdd5755bc3b213338f0e9811b6478 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 Require Import new_delete memcpy.
+From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
 From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
@@ -255,7 +255,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 ea4c662d2b558537318526dcb92b2b4bf6b46569..45a4fa0892001a011955f2bdb8d80a9fc21cc21b 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 definition of delete for
-   sets coming from the prelude. *)
-From lrust.lang Require Export new_delete.