From 4b37834a2ed6a275daec1c98fac19795f96712ce Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 18 Mar 2020 19:45:21 +0100
Subject: Interpret the Export modifier of Set and Unset as an attribute.

Unfortunately, we cannot go further and parse Export as a legacy
attribute because this syntax conflicts with the Export command.
---
 test-suite/success/attribute_syntax.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index 4717759dec..b403fc120c 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -36,3 +36,10 @@ Check M.zed@{_}.
 Fail Check zed.
 Check M.kats@{_}.
 Fail Check kats.
+
+Export Set Foo.
+
+#[ export ] Set Foo.
+
+Fail #[ export ] Export Foo.
+(* Attribute for Locality specified twice *)
-- 
cgit v1.2.3