From f3f5c57f21300ba2ca5a5bc68e082abddfcb7e1e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 22 Jun 2019 10:57:44 +0200
Subject: [PATCH] avoid using value notation for primitive operational rules

---
 theories/heap_lang/lifting.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9e5e2098c..7df887249 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -377,7 +377,7 @@ Qed.
 Lemma wp_cmpxchg_fail s E l q v' v1 v2 :
   val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
   {{{ ▷ l ↦{q} v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET (v', #false); l ↦{q} v' }}}.
+  {{{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }}}.
 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 %?.
@@ -388,7 +388,7 @@ Qed.
 Lemma twp_cmpxchg_fail s E l q v' v1 v2 :
   val_for_compare v' ≠ val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
   [[{ l ↦{q} v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET (v', #false); l ↦{q} v' }]].
+  [[{ RET PairV v' (LitV $ LitBool false); l ↦{q} v' }]].
 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 %?.
@@ -400,7 +400,7 @@ Qed.
 Lemma wp_cmpxchg_suc s E l v1 v2 v' :
   val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
   {{{ ▷ l ↦ v' }}} CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  {{{ RET (v', #true); l ↦ v2 }}}.
+  {{{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }}}.
 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 %?.
@@ -412,7 +412,7 @@ Qed.
 Lemma twp_cmpxchg_suc s E l v1 v2 v' :
   val_for_compare v' = val_for_compare v1 → vals_cmpxchg_compare_safe v' v1 →
   [[{ l ↦ v' }]] CmpXchg (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
-  [[{ RET (v', #true); l ↦ v2 }]].
+  [[{ RET PairV v' (LitV $ LitBool true); l ↦ v2 }]].
 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 %?.
-- 
GitLab