From 2a4baa1da666c4a121f383a55e07c049ea9ccdea Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Fri, 14 Oct 2016 14:20:01 +0200
Subject: [PATCH] Rename some rules : pvs -> vup.

---
 docs/program-logic.tex    | 4 ++--
 heap_lang/lib/spin_lock.v | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 868722836..77f010aea 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -230,10 +230,10 @@ The following rules can all be derived inside the DC logic:
 {\mask_1 \subseteq \mask_2 \and \vctx,\var:\textlog{val}\mid\prop \proves \propB}
 {\vctx\mid\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
 
-\infer[pvs-wp]
+\infer[vup-wp]
 {}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
 
-\infer[wp-pvs]
+\infer[wp-vup]
 {}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
 
 \infer[wp-atomic]
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 71db16199..6eb603694 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -87,6 +87,7 @@ Section proof.
     rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
     wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
   Qed.
+
 End proof.
 
 Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
-- 
GitLab