From 1889960be99572de757aa318e1f879355d60c13e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 1 Jul 2019 10:58:38 +0200
Subject: [PATCH] minor tweaks

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

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index e02449f21..1d6861cdb 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -153,7 +153,8 @@ read and written.  Also notice that the sets of boxed and unboxed values are
 disjoint. *)
 Definition lit_is_unboxed (l: base_lit) : Prop :=
   match l with
-  (* disallow comparing (erased) prophecies with (erased) prophecies, by considering them boxed *)
+  (** Disallow comparing (erased) prophecies with (erased) prophecies, by
+  considering them boxed. *)
   | LitProphecy _ | LitErased => False
   | _ => True
   end.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index a006612fa..8dda1c8f2 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -593,7 +593,7 @@ Proof.
 Qed.
 
 Lemma wp_load_offset_vec s E l sz (off : fin sz) (vs : vec val sz) :
-  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET (vs !!! off); l ↦∗ vs }}}.
+  {{{ ▷ l ↦∗ vs }}} ! #(l +ₗ off) @ s; E {{{ RET vs !!! off; l ↦∗ vs }}}.
 Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
 
 Lemma wp_store_offset s E l off vs v :
@@ -628,7 +628,7 @@ Proof.
 Qed.
 
 Lemma wp_cmpxchg_suc_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
-  (vs !!! off) = v1 →
+  vs !!! off = v1 →
   vals_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
@@ -655,7 +655,7 @@ Proof.
 Qed.
 
 Lemma wp_cmpxchg_fail_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v1 v2 :
-  (vs !!! off) ≠ v1 →
+  vs !!! off ≠ v1 →
   vals_compare_safe (vs !!! off) v1 →
   {{{ ▷ l ↦∗ vs }}}
     CmpXchg #(l +â‚— off) v1 v2 @ s; E
-- 
GitLab