1 files changed, 8 insertions, 8 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3afe3391b..e9d6ed9f6 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -83,26 +83,26 @@ GRAMMAR EXTEND Gram
     ]
   ;
   decorated_vernac:
-    [ [ a = attributes ; fv = vernac -> let (f, v) = fv in (List.append a f, v)
-      | fv = vernac -> fv ]
+    [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) }
+      | fv = vernac -> { fv } ]
     ]
   ;
   attributes:
-    [ [ "#[" ; a = attribute_list ; "]" -> a ]
+    [ [ "#[" ; a = attribute_list ; "]" -> { a } ]
     ]
   ;
   attribute_list:
-    [ [ a = LIST0 attribute SEP "," -> a ]
+    [ [ a = LIST0 attribute SEP "," -> { a } ]
     ]
   ;
   attribute:
-    [ [ k = ident ; v = attribute_value -> (Names.Id.to_string k, v) ]
+    [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ]
     ]
   ;
   attribute_value:
-    [ [ "=" ; v = string -> VernacFlagLeaf v
-      | "(" ; a = attribute_list ; ")" -> VernacFlagList a
-      | -> VernacFlagEmpty ]
+    [ [ "=" ; v = string -> { VernacFlagLeaf v }
+      | "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
+      | -> { VernacFlagEmpty } ]
     ]
   ;
   vernac: