From 3ba5fca8df0624eefc508a95c0ce1968bb10db32 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 May 2021 13:16:58 +0200
Subject: [PATCH] remove some inconsistent empty lines

---
 iris_heap_lang/derived_laws.v   | 1 -
 iris_heap_lang/primitive_laws.v | 1 -
 2 files changed, 2 deletions(-)

diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index 7e28862f3..e4e218a72 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -228,7 +228,6 @@ Proof.
   setoid_rewrite vec_to_list_insert. apply twp_xchg_offset => //.
   by apply vlookup_lookup.
 Qed.
-
 Lemma wp_xchg_offset_vec s E l sz (off : fin sz) (vs : vec val sz) v :
    {{{ ▷ l ↦∗ vs }}} Xchg #(l +ₗ off) v @ s; E {{{ RET (vs !!! off); l ↦∗ vinsert off v vs }}}.
 Proof.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 649c64383..87adf2a6b 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -323,7 +323,6 @@ Proof.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit; first done. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
-
 Lemma wp_xchg s E l v' v :
   {{{ ▷ l ↦ v' }}} Xchg (Val $ LitV (LitLoc l)) (Val v) @ s; E
   {{{ RET v'; l ↦ v }}}.
-- 
GitLab