Add test.

8845003c · Robbert Krebbers · 6106d521 · 8845003c · 8845003c
Commit 8845003c authored 2 years ago by Robbert Krebbers
--- a/tests/siprop.ref
+++ b/tests/siprop.ref
--- a/tests/siprop.v
+++ b/tests/siprop.v
+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