Commit b034fd49 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Trailing newline.

parent 82b8ee7d
Pipeline #64445 passed with stage
in 7 minutes and 33 seconds
......@@ -2,4 +2,4 @@ From iris.si_logic Require Import bi.
(** Make sure that [siProp]s are parsed in [bi_scope]. *)
Definition test : siProp := True.
Definition testI : siPropI := True.
\ No newline at end of file
Definition testI : siPropI := True.
Supports Markdown
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