diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 868722836996ce0327a493c7a68489a729b05944..77f010aea51e00b57c53b7b06e066feeb8debae4 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 71db1619931284c0285b8252ce106204cdb6ad25..6eb603694a60ebdcb491764909b68d5363b5891e 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 Σ :=