diff options
| -rw-r--r-- | vernac/g_vernac.mlg | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index ac2341ac8d..28b9fa7449 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1225,9 +1225,8 @@ GRAMMAR EXTEND Gram | s, None -> SetFormat ("text",s) end } | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at"; lev = level -> { SetItemLevel (x::l,None,lev) } - | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,lev) } - | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> - { SetItemLevel ([x],Some b,lev) } + | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind -> + { SetItemLevel ([x],b,lev) } | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) } | x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) } ] ] |