From 39e45f296afefc936e3a63836d7f56c482ddee7a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 12 Oct 2020 11:16:20 +0200
Subject: attribute #[using] for Definition and Fixpoint

---
 test-suite/success/definition_using.v | 46 +++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 test-suite/success/definition_using.v

(limited to 'test-suite/success')

diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v
new file mode 100644
index 0000000000..a8eab93404
--- /dev/null
+++ b/test-suite/success/definition_using.v
@@ -0,0 +1,46 @@
+Require Import Program.
+Axiom bogus : Type.
+
+Section A.
+Variable x : bogus.
+
+#[using="All"]
+Definition c1 : bool := true.
+
+#[using="All"]
+Fixpoint c2 n : bool :=
+  match n with
+  | O => true
+  | S p => c3 p
+  end
+with c3 n : bool :=
+  match n with
+  | O => true
+  | S p => c2 p
+end.
+
+#[using="All"]
+Definition c4 : bool. Proof. exact true. Qed.
+
+#[using="All"]
+Fixpoint c5 (n : nat) {struct n} : bool. Proof. destruct n as [|p]. exact true. exact (c5 p). Qed.
+
+#[using="All", program]
+Definition c6 : bool. Proof. exact true. Qed.
+
+#[using="All", program]
+Fixpoint c7 (n : nat) {struct n} : bool :=
+  match n with
+  | O => true
+  | S p => c7 p
+  end.
+
+End A.
+
+Check c1 : bogus -> bool.
+Check c2 : bogus -> nat -> bool.
+Check c3 : bogus -> nat -> bool.
+Check c4 : bogus -> bool.
+Check c5 : bogus -> nat -> bool.
+Check c6 : bogus -> bool.
+Check c7 : bogus -> nat -> bool.
-- 
cgit v1.2.3


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/success')

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