From 9d4b5fb1a6d0c64b5a2e4bc28880a0a35bf93dc5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 Jun 2019 23:12:47 +0200
Subject: [PATCH] make cas_offset_vec lemmas more consistent

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

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 4eb3fbd05..4414aa1de 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -586,10 +586,9 @@ Proof.
   iNext. iIntros "Hl1". iApply "HΦ". iApply "Hl2". iApply "Hl1".
 Qed.
 
-Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v' v1 v2 :
-  vs !!! off = v' →
-  val_for_compare v' = val_for_compare v1 →
-  vals_cas_compare_safe v' v1 →
+Lemma wp_cas_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
+  val_for_compare (vs !!! off) = val_for_compare v1 →
+  vals_cas_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
     CAS #(l +â‚— off) v1 v2 @ s; E
   {{{ RET #true; l ↦∗ vinsert off v2 vs }}}.
-- 
GitLab