diff --git a/opam b/opam
index 645f50a427778f79eae14d73cb96a7e446947a14..193e3a075eb0708627f9799779dac21770540aa9 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-10-25.0.bbd38120") | (= "dev") }
+  "coq-iris" { (= "dev.2019-11-07.1.891124d6") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/par.v b/theories/examples/par.v
index b23b34ef95249d1a653cc4bbc1389772f11031f0..f102f15893285f06b9744e8e05b42f7a29204e83 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -60,7 +60,7 @@ Section rules.
       iApply (refines_bind with "He").
       iIntros (v v') "Hv". simpl.
       repeat rel_pure_l.
-      rel_bind_l (join _).
+      rel_bind_l (spawn.join _).
       iApply refines_wp_l.
       iApply (join_spec with "hndl").
       iNext. iIntros (?) "_". simpl.
@@ -104,7 +104,7 @@ Section rules.
     rewrite {3}refines_eq /refines_def. iIntros (ρ) "#Hρ".
     iIntros (j K) "Hj". iModIntro.
     tp_bind j e2.
-    pose (C:=(AppRCtx (λ: "v2", let: "v1" := join #c2 in ("v1", "v2")) :: K)).
+    pose (C:=(AppRCtx (λ: "v2", let: "v1" := spawn.join #c2 in ("v1", "v2")) :: K)).
     fold C.
     pose (N:=nroot.@"par").
     wp_bind (spawn _).
@@ -119,7 +119,7 @@ Section rules.
       iMod ("He1" with "Hρ Hi") as "He1".
       iApply (wp_wand with "He1").
       iIntros (v1). iDestruct 1 as (v2) "[Hi Hv]".
-      wp_pures. wp_bind (join _).
+      wp_pures. wp_bind (spawn.join _).
       iApply (join_spec with "l_hndl").
       iNext. iIntros (w1). iDestruct 1 as (w2) "[Hj Hw]".
       unfold C. iSimpl in "Hi". iSimpl in "Hj".
@@ -128,7 +128,7 @@ Section rules.
       (* TODO: better tp_pure tactics *)
       tp_pure j (Lam _ _). simpl.
       tp_rec j. simpl.
-      tp_bind j (join _). unlock join.
+      tp_bind j (spawn.join _). unlock spawn.join.
       tp_pure j (App _ #c2). simpl.
       iApply fupd_wp. tp_load j. simpl.
       tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
@@ -172,7 +172,7 @@ Section rules.
     (* TODO: better tp_pure tactics *)
     tp_pure j (Lam _ _). simpl.
     tp_rec j. simpl.
-    tp_bind j (join _). unlock join.
+    tp_bind j (spawn.join _). unlock spawn.join.
     tp_pure j (App _ #c2). simpl.
     tp_load j. simpl.
     tp_pure j (Case _ _ _). tp_pure j (Lam _ _). simpl.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 7117295d8400d5379b601871a663842bd56dd861..e3d70b167cc0b7c32c57723837b1854de14a1ae2 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -266,7 +266,7 @@ Section proof.
       iMod (same_size with "[$Ha $Hf]") as "[Ha #Hf]".
       iMod (inc_size with "Ha") as "Ha".
       iDestruct "Hs2" as "[Hs2 Hs2']".
-      replace (m' + 1) with (Z.of_nat (S m')); last lia.
+      replace (m' + 1)%Z with (Z.of_nat (S m')); last lia.
       iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
       { iNext. iExists _,_. by iFrame. }
       rel_load_l. repeat rel_pure_l.
@@ -345,7 +345,7 @@ Section proof.
       iMod (same_size with "[$Ha $Hf]") as "[Ha #Hf]".
       iMod (inc_size with "Ha") as "Ha".
       iDestruct "Hs2" as "[Hs2 Hs2']".
-      replace (m' + 1) with (Z.of_nat (S m')); last lia.
+      replace (m' + 1)%Z with (Z.of_nat (S m')); last lia.
       iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".
       { iNext. iExists _,_. by iFrame. }
       rel_load_l. repeat rel_pure_l.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index b884eb7052ba2fe5a0950ec011fde3749352bbd2..ad6bd1e6df1bf69d39fd5060eb5eca3592f78a75 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -236,7 +236,7 @@ Section proofs.
           compute in Hfoo. eauto. }
         iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
         { iNext. iExists (S n).
-          replace (Z.of_nat (S n)) with (n + 1) by lia.
+          replace (Z.of_nat (S n)) with (n + 1)%Z by lia.
           iFrame. }
         repeat rel_pure_l. repeat rel_pure_r.
         rel_store_l_atomic. clear n'.
@@ -250,7 +250,7 @@ Section proofs.
         rel_store_r.
         iMod ("Hcl" with "[-]") as "_".
         { iNext. iExists (S n).
-          replace (Z.of_nat (S n)) with (n + 1) by lia.
+          replace (Z.of_nat (S n)) with (n + 1)%Z by lia.
           iFrame. iLeft. iFrame. }
         rel_values. }
     - rel_pure_l. rel_pure_r. iApply refines_arrow.
@@ -389,27 +389,27 @@ Section proofs.
         iApply ("Hcl" with "[-]"); iNext.
         + iExists n. iLeft. iFrame.
         + iExists (n-1)%nat. iRight.
-          replace (Z.of_nat (n-1)%nat) with (Z.of_nat n - 1) by lia.
-          replace (n - 1 + 1) with (Z.of_nat n) by lia.
+          replace (Z.of_nat (n - 1)) with (Z.of_nat n - 1)%Z by lia.
+          replace (n - 1 + 1)%Z with (Z.of_nat n) by lia.
          iFrame. }
       { iIntros "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
         - rel_apply_r (FG_increment_r with "Hc2"). iIntros "Hc2".
           iMod ("Hcl" with "[-]") as "_".
           { iNext. iExists (n + 1)%nat.
-            replace (Z.of_nat (n + 1)%nat) with (Z.of_nat n + 1) by lia.
+            replace (Z.of_nat (n + 1)) with (Z.of_nat n + 1)%Z by lia.
             iLeft; iFrame. }
           rel_values.
-        - replace (Z.of_nat n - 1) with (Z.of_nat (n - 1)%nat) by lia.
+        - replace (Z.of_nat n - 1)%Z with (Z.of_nat (n - 1)) by lia.
           rel_apply_r (FG_increment_r with "Hc2"). iIntros "Hc2".
           iMod ("Hcl" with "[-]") as "_".
           { iNext. iExists n. iRight; iFrame.
-            by replace ((n - 1)%nat + 1) with (Z.of_nat n) by lia. }
+            by replace ((n - 1)%nat + 1)%Z with (Z.of_nat n) by lia. }
          rel_values. }
-    - iModIntro. iExists (n+1)%nat.
-      replace (Z.of_nat n + 1) with (Z.of_nat (n+1)) by lia. iFrame.
+    - iModIntro. iExists (n + 1)%nat.
+      replace (Z.of_nat n + 1)%Z with (Z.of_nat (n + 1)) by lia. iFrame.
       iSplitL "Hc2 Ht".
-      { iRight. replace ((n + 1)%nat - 1) with (Z.of_nat n) by lia.
+      { iRight. replace ((n + 1)%nat - 1)%Z with (Z.of_nat n) by lia.
         iFrame. iDestruct "Ht" as "[$ $]".
         iPureIntro. lia. }
       iSplit.
@@ -418,8 +418,8 @@ Section proofs.
         + iExists (S n). iLeft.
           replace (Z.of_nat (n + 1)) with (Z.of_nat (S n)) by lia. iFrame.
         + iExists n. iRight. iFrame.
-          replace (Z.of_nat (n + 1)) with (Z.of_nat n + 1) by lia.
-          replace (n + 1 - 1) with (Z.of_nat n) by lia.
+          replace (Z.of_nat (n + 1)) with (Z.of_nat n + 1)%Z by lia.
+          replace (n + 1 - 1)%Z with (Z.of_nat n) by lia.
           iFrame. }
      { iIntros "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
@@ -427,16 +427,16 @@ Section proofs.
           iIntros "Hc2".
           iMod ("Hcl" with "[-]") as "_".
           { iNext. iExists (S (S n)).
-            replace ((n+1)%nat + 1) with (Z.of_nat (S (S n))) by lia.
+            replace ((n+1)%nat + 1)%Z with (Z.of_nat (S (S n))) by lia.
             iLeft; iFrame. }
           rel_values.
-        - replace ((n + 1)%nat + 1) with (Z.of_nat (S n) + 1) by lia.
-          replace ((n + 1)%nat - 1) with (Z.of_nat n) by lia.
+        - replace ((n + 1)%nat + 1)%Z with (Z.of_nat (S n) + 1)%Z by lia.
+          replace ((n + 1)%nat - 1)%Z with (Z.of_nat n) by lia.
           rel_apply_r (FG_increment_r with "Hc2").
           iIntros "Hc2".
           iMod ("Hcl" with "[-]") as "_".
           { iNext. iExists (S n). iRight. iFrame.
-            by replace (n + 1) with (Z.of_nat (S n)) by lia. }
+            by replace (n + 1)%Z with (Z.of_nat (S n)) by lia. }
           rel_values. }
   Qed.
 
@@ -464,8 +464,8 @@ Section proofs.
     iDestruct 1 as (m) "[Hc1 Hc2]".
     iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]";
       [iExists m; iLeft | iExists (m - 1)%nat; iRight]; iFrame.
-    replace ((m - 1)%nat + 1) with (Z.of_nat m) by lia.
-    replace (Z.of_nat (m - 1)%nat) with (Z.of_nat m - 1) by lia.
+    replace ((m - 1)%nat + 1)%Z with (Z.of_nat m) by lia.
+    replace (Z.of_nat (m - 1)) with (Z.of_nat m - 1)%Z by lia.
     iFrame.
   Qed.
 
@@ -490,7 +490,7 @@ Section proofs.
     iMod (shoot γ with "Hp") as "#Hs".
     iMod ("Hcl" with "[-]") as "_".
     { iNext. iExists m. iRight. iFrame.
-      replace (Z.of_nat (S m)) with (Z.of_nat m + 1) by lia. by iFrame. }
+      replace (Z.of_nat (S m)) with (Z.of_nat m + 1)%Z by lia. by iFrame. }
     iApply (refines_seq lrel_unit).
     { iApply (refines_app with "Hg").
       rel_values. }
@@ -551,18 +551,18 @@ Section proofs.
     iAlways.
     iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
       iModIntro; last first.
-    { iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1) by lia.
+    { iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z by lia.
       iFrame. iSplitL "Hc2 Ht Ht'2".
-      { iRight. simpl. replace (n + 1 - 1) with (Z.of_nat n) by lia.
-        iFrame. iPureIntro. omega. }
+      { iRight. simpl. replace (n + 1 - 1)%Z with (Z.of_nat n) by lia.
+        iFrame. iPureIntro. lia. }
       iSplit.
       - iIntros. iApply "Hcl". iApply close_i6.
-        iNext. iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1) by lia.
+        iNext. iExists (S n). replace (Z.of_nat (S n)) with (Z.of_nat n + 1)%Z by lia.
         iFrame.
       - iIntros "[Hc1 Hc2] Ht".
         rel_pure_l. rel_pure_l.
-        replace (n + 1 + 1) with (Z.of_nat (S (S n))) by lia.
-        replace (n + 1) with (Z.of_nat (S n)) by lia.
+        replace (n + 1 + 1)%Z with (Z.of_nat (S (S n))) by lia.
+        replace (n + 1)%Z with (Z.of_nat (S n)) by lia.
         iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
     }
     { iExists n. iFrame "Hc1". iSplitL "Hc2 Ht".
@@ -572,7 +572,7 @@ Section proofs.
         iNext. iExists _; iFrame.
       - iIntros  "[Hc1 Hc2] Ht".
         rel_pure_l. rel_pure_l.
-        replace (n + 1) with (Z.of_nat (S n)) by lia.
+        replace (n + 1)%Z with (Z.of_nat (S n)) by lia.
         iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
     }
   Qed.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index caa09741cba367492c21e53217a29e4efee8aebe..5e771d399f7acb01b15133aaf2850e644ccfe556 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -67,7 +67,7 @@ Theorem refines_typesafety Σ `{relocPreG Σ} e e' e1
         (A : ∀ `{relocG Σ}, lrel Σ) thp σ σ' :
   (∀ `{relocG Σ}, REL e << e' : A) →
   rtc erased_step ([e], σ) (thp, σ') → e1 ∈ thp →
-  is_Some (to_val e1) ∨ reducible e1 σ'.
+  not_stuck e1 σ'.
 Proof.
   intros Hlog ??.
   cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h) ∧ True)); first (intros [_ ?]; eauto).
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 9f481b0597c0562ea117ae70ba0579c7a4a3b7bf..e56bdb60a5833d443b3b0eab654f9a8c5bb1c96b 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -81,7 +81,7 @@ Section conversions.
   Qed.
   Lemma tpool_lookup_Some tp j e : to_tpool tp !! j = Excl' e → tp !! j = Some e.
   Proof. rewrite tpool_lookup fmap_Some. naive_solver. Qed.
-  Hint Resolve tpool_lookup_Some.
+  Hint Resolve tpool_lookup_Some : core.
 
   Lemma to_tpool_insert tp j e :
     j < length tp →
diff --git a/theories/prelude/asubst.v b/theories/prelude/asubst.v
index 15e1b7c316f8af8ef059b220808f2bb690ce0305..a53f6b9941d75326c93a0c2912bb57cd4a07bfde 100644
--- a/theories/prelude/asubst.v
+++ b/theories/prelude/asubst.v
@@ -1,9 +1,6 @@
 (** Autosubst helper lemmata *)
-From stdpp Require Export base numbers.
-From Coq.ssr Require Export ssreflect.
-Global Open Scope general_if_scope.
-(* ^ otherwise ssreflects overwrites `if` *)
 From Autosubst Require Export Autosubst.
+From iris.algebra Require Export base.
 
 Section Autosubst_Lemmas.
   Context {term : Type} {Ids_term : Ids term}
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 40dc4786faef1b96bd35741b6a0d3941abc3bf03..7ff8d31cb7f62e7f3d4ca8e6094d8cb2e3364817 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -1,11 +1,10 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Notion of contextual refinement & proof that it is a precongruence wrt the logical relation *)
+From Autosubst Require Import Autosubst.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From reloc.typing Require Export types interp fundamental.
 
-From Autosubst Require Import Autosubst.
-
 Inductive ctx_item :=
   (* λ-rec *)
   | CTX_Rec (f x: binder)
@@ -155,7 +154,7 @@ Inductive typed_ctx_item :
   | TP_CTX_Unfold Γ τ :
      typed_ctx_item CTX_Unfold Γ (TRec τ) Γ τ.[(TRec τ)/]
   | TP_CTX_TLam Γ τ :
-     typed_ctx_item CTX_TLam (subst (ren (+1%nat)) <$> Γ) τ Γ (TForall τ)
+     typed_ctx_item CTX_TLam (Autosubst_Classes.subst (ren (+1%nat)) <$> Γ) τ Γ (TForall τ)
   | TP_CTX_TApp Γ τ τ' :
      typed_ctx_item CTX_TApp Γ (TForall τ) Γ τ.[τ'/]
   (* | TP_CTX_Pack Γ τ τ' : *)
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 21cf35ae38166299742d6b1d2b2aa0df90a3b2bd..8db15c5f1e51c45438edb6433fa6ed6391382d53 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -1,11 +1,11 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Interpretations for System F_mu_ref types *)
+From Autosubst Require Import Autosubst.
 From iris.algebra Require Export list.
 From iris.proofmode Require Import tactics.
 From reloc.typing Require Export types.
 From reloc.logic Require Import model.
 From reloc.prelude Require Import properness asubst.
-From Autosubst Require Import Autosubst.
 
 (** * Interpretation of types *)
 Section semtypes.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index e22a0b8870dff1781aa501a2f170ff2fb08694b6..5a22da8f8e5b11524e6fb2ff0966bc3d1656648f 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -27,7 +27,7 @@ Qed.
 Theorem logrel_typesafety Σ `{relocPreG Σ} e e' τ thp σ σ' :
   (∀ `{relocG Σ} Δ, {⊤;Δ;∅} ⊨ e ≤log≤ e : τ) →
   rtc erased_step ([e], σ) (thp, σ') → e' ∈ thp →
-  is_Some (to_val e') ∨ reducible e' σ'.
+  not_stuck e' σ'.
 Proof.
   intros Hlog ??.
   cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))); first (intros [_ ?]; eauto).
diff --git a/theories/typing/types.v b/theories/typing/types.v
index ecc67ba81b00e8d81581c34e45e7b5384377b592..b2fa1d2bd56d6a43990e9650b14921d536ccc6be 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -1,8 +1,8 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** (Syntactic) Typing for System F_mu_ref with existential types and concurrency *)
+From Autosubst Require Export Autosubst.
 From stdpp Require Export stringmap.
 From iris.heap_lang Require Export lang notation metatheory.
-From Autosubst Require Export Autosubst.
 
 (** * Types *)
 Inductive type :=
@@ -143,7 +143,7 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
   | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/] → Γ ⊢ₜ e : TExists τ
   | TUnpack e1 x e2 Ï„ Ï„2 :
       Γ ⊢ₜ e1 : TExists τ →
-      <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (subst (ren (+1%nat)) τ2) →
+      <[x:=τ]>(⤉ Γ) ⊢ₜ e2 : (Autosubst_Classes.subst (ren (+1%nat)) τ2) →
       Γ ⊢ₜ (unpack: x := e1 in e2) : τ2
   | TFork e : Γ ⊢ₜ e : TUnit → Γ ⊢ₜ Fork e : TUnit
   | TAlloc e τ : Γ ⊢ₜ e : τ → Γ ⊢ₜ Alloc e : Tref τ