diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1aff76114b..d9b664e243 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -119,7 +119,8 @@ GRAMMAR EXTEND Gram ] ; attr_value: - [ [ "=" ; v = string -> { VernacFlagLeaf v } + [ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) } + | "=" ; v = IDENT -> { VernacFlagLeaf (FlagIdent v) } | "(" ; a = attribute_list ; ")" -> { VernacFlagList a } | -> { VernacFlagEmpty } ] ] |