Commit 3a0d7152 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove redundant space.

parent ed3b52f9
......@@ -60,7 +60,7 @@ Implicit Types e : expr Λ.
(* Weakest pre *)
Lemma wp_unfold s E e Φ :
WP e @ s; E {{ Φ }} wp_pre s (wp (PROP:=iProp Σ) s) E e Φ.
WP e @ s; E {{ Φ }} wp_pre s (wp (PROP:=iProp Σ) s) E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
Global Instance wp_ne s E e n :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment