From 1a4d29ea194833d337ff23320c56e7f324fa82b7 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 3 Jul 2018 16:25:52 +0000
Subject: fix syntax of .mlg

---
 vernac/g_vernac.mlg | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'vernac')

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:
-- 
cgit v1.2.3