From 420b38cba7aedfcfeac5671a7db0c02c4bb14a0c Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 3 Jul 2018 17:06:03 +0000
Subject: [test suite] Test case for attributes

---
 test-suite/success/attribute-syntax.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 test-suite/success/attribute-syntax.v

(limited to 'test-suite/success')

diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
new file mode 100644
index 000000000..83fb3d0c8
--- /dev/null
+++ b/test-suite/success/attribute-syntax.v
@@ -0,0 +1,23 @@
+From Coq Require Program.
+
+Section Scope.
+
+#[local] Coercion nat_of_bool (b: bool) : nat :=
+  if b then 0 else 1.
+
+Check (refl_equal : true = 0 :> nat).
+
+End Scope.
+
+Fail Check 0 = true :> nat.
+
+#[polymorphic]
+Definition ι T (x: T) := x.
+
+Check ι _ ι.
+
+#[program]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+
+#[deprecated(since="8.9.0")]
+Ltac foo := foo.
-- 
cgit v1.2.3