From 697bfeba6f5bdff48b254092a3f7f6616080e9b2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 19 Sep 2018 13:42:44 +0200
Subject: Allow successive attributes #[foo] #[bar]

---
 vernac/g_vernac.mlg | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 650b28ea67..7dd5471f3f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -83,11 +83,10 @@ GRAMMAR EXTEND Gram
     ]
   ;
   decorated_vernac:
-    [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) }
-      | fv = vernac -> { fv } ]
-    ]
+    [ [ a = LIST0 quoted_attributes ; fv = vernac ->
+        { let (f, v) = fv in (List.append (List.flatten a) f, v) } ] ]
   ;
-  attributes:
+  quoted_attributes:
     [ [ "#[" ; a = attribute_list ; "]" -> { a } ]
     ]
   ;
-- 
cgit v1.2.3