From 8845003c64768ab034571210749e7d87d9de18f9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Apr 2022 22:16:32 +0200
Subject: [PATCH] Add test.

---
 tests/siprop.ref | 0
 tests/siprop.v   | 5 +++++
 2 files changed, 5 insertions(+)
 create mode 100644 tests/siprop.ref
 create mode 100644 tests/siprop.v

diff --git a/tests/siprop.ref b/tests/siprop.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/siprop.v b/tests/siprop.v
new file mode 100644
index 000000000..da5fc4be4
--- /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
-- 
GitLab