diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:25:52 +0000 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:25:52 +0000 |
commit | 1a4d29ea194833d337ff23320c56e7f324fa82b7 (patch) | |
tree | 0e5da8f2df16a904f60b9378d8d1c2d0aa8e1fae /vernac | |
parent | 1615f76645b0307485ee3143b0d185e91a4935b5 (diff) |
fix syntax of .mlg
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/g_vernac.mlg | 16 |
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: |