diff --git a/tests/siprop.ref b/tests/siprop.ref new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/siprop.v b/tests/siprop.v new file mode 100644 index 0000000000000000000000000000000000000000..da5fc4be47da6a3e853dc5967b065a8f5993e494 --- /dev/null +++ b/tests/siprop.v @@ -0,0 +1,5 @@ +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