diff options
| author | Hugo Herbelin | 2020-02-10 17:37:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-16 21:44:43 +0100 |
| commit | cb3744bbf5165851877e17c12e92b40027526a04 (patch) | |
| tree | 87752098122f2a08c7a245d9e95c37aab6ec284d | |
| parent | 6eb4dbf6ba77ae7e9087832ea1e27426b515a8e8 (diff) | |
Mini-factorization in vernac grammar.
Unfortunately, we cannot factorize further
| x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind
| x = IDENT; b = constr_as_binder_kind
without losing the rule
| x = IDENT; typ = syntax_extension_type
| -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) } ] ] |