diff --git a/opam b/opam
index 18a6991dec221eb57850b3c771f9ea4d039370c6..25ea28e3043bf5144e5def6f05256b96250203c4 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-24.3.5ef58527") | (= "dev") }
+  "coq-iris" { (= "dev.2019-07-01.1.6e79f000") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index e70020083ce2e9868defdec46dd4e2d2458305a2..ed19fff77ff5d122d98479b2053688588ce6a026 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -245,10 +245,10 @@ Section refinement.
   Local Instance oloc_to_val_inj : Inj (=) (=) oloc_to_val.
   Proof. intros [|][|]; simpl; congruence. Qed.
 
-  Notation D := (olocO -n> valO -n> iProp Σ).
+  Notation D := (olocO -d> valO -d> iProp Σ).
 
-  Program Definition stack_link_pre : D -> D := λ S, λne ol v2,
-    match ol with
+  Definition stack_link_pre : D → D := λ S ol v2,
+    match ol return _ with
     | None => ⌜v2 = NONEV⌝
     | Some l => ∃ (h : val) (t : option loc) (h' t' : val),
                   ⌜v2 = SOMEV (h', t')⌝
@@ -258,13 +258,9 @@ Section refinement.
 
   Global Instance stack_link_pre_contractive : Contractive stack_link_pre.
   Proof.
-    solve_proper_prepare. destruct x0; last done.
-    repeat (first [eassumption | f_contractive | f_equiv]).
+    intros n S1 S2 HS. solve_proper_prepare.
+    repeat (first [apply HS | f_contractive | f_equiv]).
   Qed.
-
-  Global Instance stack_link_pre_ne : NonExpansive stack_link_pre.
-  Proof. apply contractive_ne, _. Qed.
-
   Definition stack_link := fixpoint stack_link_pre.
 
   Lemma stack_link_unfold ol v2 :
@@ -276,12 +272,7 @@ Section refinement.
                  ∗ (∃ q, l ↦{q} (h, oloc_to_val t))
                  ∗ lrel_int h h' ∗ ▷ stack_link t t'
      end%I).
-  Proof.
-    rewrite {1}/stack_link.
-    transitivity (stack_link_pre (fixpoint stack_link_pre) ol v2).
-    { f_equiv. f_equiv. apply fixpoint_unfold. }
-    destruct ol; reflexivity.
-  Qed.
+  Proof. apply (fixpoint_unfold stack_link_pre). Qed.
 
   Lemma stack_link_empty : stack_link None NILV.
   Proof. rewrite stack_link_unfold; by iPureIntro. Qed.
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 3ebd7e4b6c7bee518f40a73f7ae7d581ef93a5fd..45fbfffbd8b3335775da362894949d731c33ab37 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -257,8 +257,8 @@ Lemma tac_tp_cmpxchg_fail `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l
   IntoVal e1 v1 →
   IntoVal e2 v2 →
   envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v')%I →
-  val_for_compare v' ≠ val_for_compare v1 →
-  vals_cmpxchg_compare_safe v' v1 →
+  v' ≠ v1 →
+  vals_compare_safe v' v1 →
   envs_simple_replace i3 false
     (Esnoc (Esnoc Enil i2 (j ⤇ fill K' (v', #false)%V)) i3 (l ↦ₛ{q} v')%I) Δ2 = Some Δ3 →
   envs_entails Δ3 (|={E1,E2}=> Q) →
@@ -301,7 +301,7 @@ Tactic Notation "tp_cmpxchg_fail" constr(j) :=
     |iSolveTC
     |iAssumptionCore || fail "tp_cmpxchg_fail: cannot find '? ↦ ?'"
     |try (simpl; congruence) (* v' ≠ v1 *)
-    |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
+    |try heap_lang.proofmode.solve_vals_compare_safe
     |pm_reflexivity || fail "tp_cmpxchg_fail: this should not happen"
     |(* new goal *)]).
 
@@ -313,8 +313,8 @@ Lemma tac_tp_cmpxchg_suc `{relocG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e (l
   IntoVal e1 v1 →
   IntoVal e2 v2 →
   envs_lookup i3 Δ2 = Some (false, l ↦ₛ v')%I →
-  val_for_compare v' = val_for_compare v1 →
-  vals_cmpxchg_compare_safe v' v1 →
+  v' = v1 →
+  vals_compare_safe v' v1 →
   envs_simple_replace i3 false
     (Esnoc (Esnoc Enil i2 (j ⤇ fill K' (v', #true)%V)) i3 (l ↦ₛ v2)%I) Δ2 = Some Δ3 →
   envs_entails Δ3 (|={E1,E2}=> Q) →
@@ -357,7 +357,7 @@ Tactic Notation "tp_cmpxchg_suc" constr(j) :=
     |iSolveTC
     |iAssumptionCore || fail "tp_cmpxchg_suc: cannot find '? ↦ ?'"
     |try (simpl; congruence)     (* v' = v1 *)
-    |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
+    |try heap_lang.proofmode.solve_vals_compare_safe
     |pm_reflexivity || fail "tp_cmpxchg_suc: this should not happen"
     |(* new goal *)]).
 
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 47ca029438f0ee3f66a12eb80d3977df7f9e90a5..511e379d3588a782849d1f394355a802316fca73 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -102,7 +102,7 @@ Tactic Notation "rel_apply_l" open_constr(lem) :=
       end));
   try lazymatch goal with
   | |- val_is_unboxed _ => fast_done
-  | |- vals_cmpxchg_compare_safe _ _ =>
+  | |- vals_compare_safe _ _ =>
     fast_done || (left; fast_done) || (right; fast_done)
   end;
   try rel_finish.
@@ -174,7 +174,7 @@ Tactic Notation "rel_pure_l" open_constr(ef) :=
       eapply (tac_rel_pure_l K e');
       [reflexivity                  (** e = fill K e1 *)
       |iSolveTC                     (** PureClosed Ï• e1 e2 *)
-      |try fast_done                (** φ *)
+      |try heap_lang.proofmode.solve_vals_compare_safe                (** φ *)
       |first [left; split; reflexivity              (** Here we decide if the mask E is ⊤ *)
              | right; reflexivity]                  (**    (m = n ∧ E = ⊤) ∨ (m = 0) *)
       |iSolveTC                                     (** IntoLaters *)
@@ -191,7 +191,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
       eapply (tac_rel_pure_r K e');
       [reflexivity                  (** e = fill K e1 *)
       |iSolveTC                     (** PureClosed Ï• e1 e2 *)
-      |try fast_done                (** φ *)
+      |try heap_lang.proofmode.solve_vals_compare_safe                (** φ *)
       |solve_ndisj        || fail 1 "rel_pure_r: cannot solve ↑specN ⊆ ?"
       |simpl; reflexivity           (** eres = fill K e2 *)
       |rel_finish                   (** new goal *)])
@@ -438,8 +438,8 @@ Lemma tac_rel_cmpxchg_fail_r `{relocG Σ} K ℶ1 i1 E (l : loc) e1 e2 v1 v2 v e
   IntoVal e2 v2 →
   nclose specN ⊆ E →
   envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
-  val_for_compare v ≠ val_for_compare v1 →
-  vals_cmpxchg_compare_safe v v1 →
+  v ≠ v1 →
+  vals_compare_safe v v1 →
   eres = fill K (v, #false)%V →
   envs_entails ℶ1 (refines E t eres A) →
   envs_entails ℶ1 (refines E t e A).
@@ -457,8 +457,8 @@ Lemma tac_rel_cmpxchg_suc_r `{relocG Σ} K ℶ1 ℶ2 i1 E (l : loc) e1 e2 v1 v2
   IntoVal e2 v2 →
   nclose specN ⊆ E →
   envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
-  val_for_compare v = val_for_compare v1 →
-  vals_cmpxchg_compare_safe v v1 →
+  v = v1 →
+  vals_compare_safe v v1 →
   envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v2)) ℶ1 = Some ℶ2 →
   eres = fill K (v, #true)%V →
   envs_entails ℶ2 (refines E t eres A) →
@@ -489,7 +489,7 @@ Tactic Notation "rel_cmpxchg_fail_r" :=
   [solve_ndisj || fail "rel_cmpxchg_fail_r: cannot prove 'nclose specN ⊆ ?'"
   |solve_mapsto ()
   |try (simpl; congruence)   (** v ≠ v1 *)
-  |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
+  |try heap_lang.proofmode.solve_vals_compare_safe
   |reflexivity
   |rel_finish  (** new goal *)].
 
@@ -510,7 +510,7 @@ Tactic Notation "rel_cmpxchg_suc_r" :=
   [solve_ndisj || fail "rel_cmpxchg_suc_r: cannot prove 'nclose specN ⊆ ?'"
   |solve_mapsto ()
   |try (simpl; congruence)   (** v = v1 *)
-  |try heap_lang.proofmode.solve_vals_cmpxchg_compare_safe
+  |try heap_lang.proofmode.solve_vals_compare_safe
   |pm_reflexivity  (** new env *)
   |reflexivity
   |rel_finish  (** new goal *)].
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 8ce5ee8fdba1413e6fa83c7543bf6a1701ef6d51..d5392c37cd671daae3e74a0659b0fe3cb9db7656 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -198,8 +198,8 @@ Section rules.
     nclose specN ⊆ E →
     IntoVal e1 v1 →
     IntoVal e2 v2 →
-    vals_cmpxchg_compare_safe v v1 →
-    val_for_compare v ≠ val_for_compare v1 →
+    vals_compare_safe v v1 →
+    v ≠ v1 →
     l ↦ₛ v -∗
     (l ↦ₛ v -∗ REL t << fill K (of_val (v, #false)) @ E : A)
     -∗ REL t << fill K (CmpXchg #l e1 e2) @ E : A.
@@ -220,8 +220,8 @@ Section rules.
     nclose specN ⊆ E →
     IntoVal e1 v1 →
     IntoVal e2 v2 →
-    vals_cmpxchg_compare_safe v v1 →
-    val_for_compare v = val_for_compare v1 →
+    vals_compare_safe v v1 →
+    v = v1 →
     l ↦ₛ v -∗
     (l ↦ₛ v2 -∗ REL t << fill K (of_val (v, #true)) @ E : A)
     -∗ REL t << fill K (CmpXchg #l e1 e2) @ E : A.
@@ -390,14 +390,14 @@ Section rules.
     IntoVal e2 v2 →
     val_is_unboxed v1 →
     (|={⊤,E}=> ∃ v', ▷ l ↦ v' ∗
-     (⌜val_for_compare v' ≠ val_for_compare v1⌝ -∗ ▷ (l ↦ v' -∗ REL fill K (of_val (v', #false)) << t @ E : A)) ∧
-     (⌜val_for_compare v' = val_for_compare v1⌝ -∗ ▷ (l ↦ v2 -∗ REL fill K (of_val (v', #true)) << t @ E : A)))
+     (⌜v' ≠ v1⌝ -∗ ▷ (l ↦ v' -∗ REL fill K (of_val (v', #false)) << t @ E : A)) ∧
+     (⌜v' = v1⌝ -∗ ▷ (l ↦ v2 -∗ REL fill K (of_val (v', #true)) << t @ E : A)))
     -∗ REL fill K (CmpXchg #l e1 e2) << t : A.
   Proof.
     iIntros (<-<-?) "Hlog".
     iApply refines_atomic_l; auto.
     iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
-    destruct (decide (val_for_compare v' = val_for_compare v1)).
+    destruct (decide (v' = v1)).
     - (* CmpXchg successful *) subst.
       iApply (wp_cmpxchg_suc with "Hl"); eauto.
       { by right. }
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index cdb6107ad84f2c08d054ea3dabf90aaae3310a80..2db07ac771eea6b8395da192a3096d1bb9f416ed 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -217,8 +217,8 @@ Section rules.
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     nclose specN ⊆ E →
-    vals_cmpxchg_compare_safe v' v1 →
-    val_for_compare v' ≠ val_for_compare v1 →
+    vals_compare_safe v' v1 →
+    v' ≠ v1 →
     spec_ctx ρ ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ{q} v'
     ={E}=∗ j ⤇ fill K (v', #false)%V ∗ l ↦ₛ{q} v'.
   Proof.
@@ -243,8 +243,8 @@ Section rules.
     IntoVal e1 v1 →
     IntoVal e2 v2 →
     nclose specN ⊆ E →
-    vals_cmpxchg_compare_safe v1' v1 →
-    val_for_compare v1' = val_for_compare v1 →
+    vals_compare_safe v1' v1 →
+    v1' = v1 →
     spec_ctx ρ ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ v1'
     ={E}=∗ j ⤇ fill K (v1', #true)%V ∗ l ↦ₛ v2.
   Proof.
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index 836405dc27daeb197afa09f6c5d773d0d010e090..862224036833b2e89cb6ddf4c4ad3fbbe4321904 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -295,7 +295,7 @@ Section fundamental.
     simplify_eq. rel_cmpxchg_l_atomic.
     iInv (relocN .@ "ref" .@ (l,l')) as (v1 v1') "[Hv1 [>Hv2 #Hv]]" "Hclose".
     iModIntro. iExists _; iFrame. simpl.
-    destruct (decide (val_for_compare v1 = val_for_compare v2')) as [|Hneq]; subst.
+    destruct (decide (v1 = v2')) as [|Hneq]; subst.
     - iSplitR; first by (iIntros (?); contradiction).
       iIntros (?). iNext. iIntros "Hv1".
       iDestruct (eq_type_sound with "Hv") as "%"; first fast_done.