From eafd77e65aa49afc3e2cfaab4cc3d833eec9d6f5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 Jun 2019 16:09:53 +0200
Subject: [PATCH] use equality instead of let binding

---
 theories/heap_lang/lang.v    | 4 ++--
 theories/heap_lang/lifting.v | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index ea963e3ea..4a9272d89 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -634,11 +634,11 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV LitUnit) (state_upd_heap <[l:=v]> σ)
                []
-  | CompareExchangeS l v1 v2 vl σ :
+  | CompareExchangeS l v1 v2 vl σ b :
      vals_cas_compare_safe vl v1 →
      σ.(heap) !! l = Some vl →
      (* Crucially, this compares the same way as [EqOp]! *)
-     let b := bool_decide (val_for_compare vl = val_for_compare v1) in
+     b = bool_decide (val_for_compare vl = val_for_compare v1) →
      head_step (CompareExchange (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
                []
                (Val $ PairV (LitV $ LitBool b) vl) (if b then state_upd_heap <[l:=v2]> σ else σ)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index f7abd0bb6..b2ac33269 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -382,7 +382,7 @@ Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
-  rewrite /b bool_decide_false //.
+  rewrite bool_decide_false //.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_fail s E l q v' v1 v2 :
@@ -393,7 +393,7 @@ Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
-  rewrite /b bool_decide_false //.
+  rewrite bool_decide_false //.
   iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
@@ -405,7 +405,7 @@ Proof.
   iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
-  rewrite /b bool_decide_true //.
+  rewrite bool_decide_true //.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
 Qed.
@@ -417,7 +417,7 @@ Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
-  rewrite /b bool_decide_true //.
+  rewrite bool_decide_true //.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
-- 
GitLab