diff --git a/opam b/opam
index 421efdf5e1da0f99249b156aefb16bf9abc22663..4d3fe01d5998ae338b7e9c4c3fc16c8aa5a44a43 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-06-01.2.88c7fc6d") | (= "dev") }
+  "coq-iris" { (= "dev.2019-06-03.2.b368c861") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 2e9c2fdaa52d5b82828e60d1ea3b8ba8aa6e33b6..5a42d2f84ff4682dcf5a21a4147c31550a544162 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -59,8 +59,8 @@ Section proofs.
 
   (** Lazy coin (with prophecies) refines eager coin *)
   Definition I (cl ce : loc) (p : proph_id) :=
-    (∃ vs : list val, proph p vs ∗
-    (cl ↦ NONEV ∗ ce ↦ₛ #(val_to_bool vs)
+    (∃ vs : list (val*val), proph p vs ∗
+    (cl ↦ NONEV ∗ ce ↦ₛ #(extract_bool vs)
     ∨ ∃ (b:bool), cl ↦ SOMEV #b ∗ ce ↦ₛ #b))%I.
 
   Lemma coin_lazy'_eager_refinement :
@@ -105,12 +105,12 @@ Section proofs.
       iDestruct 1 as (vs) "[Hp H]". repeat rel_pure_l.
       iDestruct "H" as "[[Hcl Hce]|H]"; last iDestruct "H" as (x) "[Hcl Hce]";
         rel_store_l; repeat rel_pure_l.
-      + rel_apply_r (refines_rand_r (val_to_bool vs)).
+      + rel_apply_r (refines_rand_r (extract_bool vs)).
         rel_store_r.
         rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
         { iExists vs. iFrame. iLeft. iFrame. }
         iNext. rel_values.
-      + rel_apply_r (refines_rand_r (val_to_bool vs)).
+      + rel_apply_r (refines_rand_r (extract_bool vs)).
         rel_store_r.
         rel_apply_l (refines_release_l with "Hlk Hlocked [-]").
         { iExists vs. iFrame. iLeft. iFrame. }
diff --git a/theories/examples/lateearlychoice.v b/theories/examples/lateearlychoice.v
index 029080aa263aa1227e226f882ffda1daa71c16ef..226a584806da4ecff473b138b6178e6ab27b4204 100644
--- a/theories/examples/lateearlychoice.v
+++ b/theories/examples/lateearlychoice.v
@@ -62,9 +62,9 @@ Section proof.
       iMod ("Hcl" with "[Hy]") as "_"; eauto with iFrame.
   Qed.
 
-  Definition val_to_bool (vs : list val) : bool :=
+  Definition extract_bool (vs : list (val*val)) : bool :=
     match vs with
-    | LitV (LitBool b)::_ => b
+    | (_,LitV (LitBool b))::_ => b
     | _                   => true
     end.
 
@@ -77,7 +77,7 @@ Section proof.
     rel_rec_l. rel_rec_r.
     rel_newproph_l vs p as "Hp".
     repeat rel_pure_l.
-    rel_apply_r (refines_rand_r (val_to_bool vs)).
+    rel_apply_r (refines_rand_r (extract_bool vs)).
     repeat rel_pure_r.
     iApply (refines_seq lrel_unit).
     { iApply refines_store.
diff --git a/theories/examples/or.v b/theories/examples/or.v
index a0562e26d7393deb9e5c862bd02e483ac4ae3417..080b9ff173f33e56d3b8d6ba338cc99428f0378e 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** (In)equational theory of erratic choice operator (`or`). *)
-From reloc Require Export reloc lib.Y (* for bot *).
+From reloc Require Export reloc lib.Y. (* for bot *)
 Set Default Proof Using "Type".
 
 (** (Binary) non-determinism can be simluated with concurrency. In
@@ -221,9 +221,9 @@ Section rules.
   (** To prove the refinement in the other direction, we instrument
   our program with prophecies and resolve them when we actually make
   the choice on the LHS *)
-  Definition to_choice (vs : list val) : bool :=
+  Definition to_choice (vs : list (val*val)) : bool :=
     match vs with
-    | LitV (LitInt 0)::_ => true
+    | (_,LitV (LitInt 0))::_ => true
     | _ => false
     end.
 
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 19869906250e7fb4e99166a28e58cca9366b1b71..683799bf5b9494f866abe0939ed32371351f6782 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -521,7 +521,7 @@ Tactic Notation "rel_newproph_l_atomic" := rel_apply_l refines_newproph_l.
 Lemma tac_rel_newproph_l_simpl `{relocG Σ} K ℶ1 ℶ2 e t A :
   e = fill K NewProph →
   MaybeIntoLaterNEnvs 1 ℶ1 ℶ2 →
-  (envs_entails ℶ2 (∀ (vs : list val) (p : proph_id),
+  (envs_entails ℶ2 (∀ (vs : list (val*val)) (p : proph_id),
      (proph p vs -∗ refines ⊤ (fill K (of_val #p)) t A))) →
   envs_entails ℶ1 (refines ⊤ e t A).
 Proof.
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index e77ff8c641fbfdc875aefb08102ab68dd0cb1ab5..e8f213f6bf655884979f96fb12650e09baf44255 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -335,7 +335,7 @@ Section rules.
   Qed.
 
   Lemma refines_newproph_l K E t A :
-    (|={⊤,E}=> ▷ (∀ (vs : list val) (p : proph_id),
+    (|={⊤,E}=> ▷ (∀ (vs : list (val*val)) (p : proph_id),
            proph p vs -∗
            REL fill K (of_val #p) << t @ E : A))%I
     -∗ REL fill K NewProph << t : A.
@@ -349,7 +349,7 @@ Section rules.
   Lemma refines_resolveproph_l K E (p : proph_id) w t A :
     (|={⊤,E}=> ∃ vs,
            ▷ (proph p vs) ∗
-           ▷ (∀ (vs' : list val), ⌜vs = w::vs'⌝ -∗
+           ▷ (∀ (vs' : list (val*val)), ⌜vs = (LitV LitUnit,w)::vs'⌝ -∗
                   proph p vs' -∗
                   REL fill K (of_val #()) << t @ E : A))%I
     -∗ REL fill K (ResolveProph #p w) << t : A.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 78b0437a69de4265b8ca66e9a7926ac6266a13ac..08e4a315bc108e196407dcc60026e02cc328ecbc 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -134,6 +134,7 @@ Section rules.
     iExists (<[j:=fill K #()]> tp), σ.
     rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+    econstructor; eauto.
   Qed.
 
   (** Alloc, load, and store *)
@@ -320,4 +321,3 @@ Section rules.
   Qed.
 
 End rules.
-
diff --git a/theories/prelude/ctx_subst.v b/theories/prelude/ctx_subst.v
index 8b633b66defe8cf1503973dbd2d0916b4a69e70e..a69e74e4ae3ed483cd24cfd39543ab17d56d2139 100644
--- a/theories/prelude/ctx_subst.v
+++ b/theories/prelude/ctx_subst.v
@@ -29,8 +29,9 @@ Fixpoint subst_map_ctx_item (es : stringmap val) (K : ectx_item)
   | CasRCtx e0 e1 => CasRCtx (subst_map es e0) (subst_map es e1)
   | FaaLCtx v2 => FaaLCtx v2
   | FaaRCtx e1 => FaaRCtx (subst_map es e1)
-  | ProphLCtx v2 => ProphLCtx v2
-  | ProphRCtx e1 => ProphRCtx (subst_map es e1)
+  | ResolveLCtx Ki v1 v2 => ResolveLCtx (subst_map_ctx_item es Ki) v1 v2
+  | ResolveMCtx e0 v2 => ResolveMCtx (subst_map es e0) v2
+  | ResolveRCtx e0 e1 => ResolveRCtx (subst_map es e0) (subst_map es e1)
   end.
 
 Definition subst_map_ctx (es : stringmap val) (K : list ectx_item) :=
@@ -39,7 +40,7 @@ Definition subst_map_ctx (es : stringmap val) (K : list ectx_item) :=
 Lemma subst_map_fill_item (vs : stringmap val) (Ki : ectx_item) (e : expr)  :
   subst_map vs (fill_item Ki e) =
   fill_item (subst_map_ctx_item vs Ki) (subst_map vs e).
-Proof. induction Ki; simpl; eauto. Qed.
+Proof. induction Ki; simpl; eauto with f_equal. Qed.
 
 Lemma subst_map_fill (vs : stringmap val) (K : list ectx_item) (e : expr) :
   subst_map vs (fill K e) = fill (subst_map_ctx vs K) (subst_map vs e).