Commit d35e4c0d authored by Robbert Krebbers's avatar Robbert Krebbers

Add duplicate new line at end of file.

parent 8bccbcc9
...@@ -400,4 +400,3 @@ Section proofmode_classes. ...@@ -400,4 +400,3 @@ Section proofmode_classes.
(WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100. (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed. Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes. End proofmode_classes.
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