From fd9d10f2c7eff9ff72f42e9ecd3ffd5179de4da0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 12 Oct 2020 16:52:47 +0200
Subject: [stm] support #[using] attribute

---
 test-suite/success/definition_using.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v
index a8eab93404..120e62b145 100644
--- a/test-suite/success/definition_using.v
+++ b/test-suite/success/definition_using.v
@@ -44,3 +44,25 @@ Check c4 : bogus -> bool.
 Check c5 : bogus -> nat -> bool.
 Check c6 : bogus -> bool.
 Check c7 : bogus -> nat -> bool.
+
+Section B.
+
+Variable a : bogus.
+Variable h : c1 a = true.
+
+#[using="a*"]
+Definition c8 : bogus := a.
+
+Collection ccc := a h.
+
+#[using="ccc"]
+Definition c9 : bogus := a.
+
+#[using="ccc - h"]
+Definition c10 : bogus := a.
+
+End B.
+
+Check c8 : forall a, c1 a = true -> bogus.
+Check c9 : forall a, c1 a = true -> bogus.
+Check c10: bogus -> bogus.
-- 
cgit v1.2.3