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 /kernel/type_errors.mli | |
| 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
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions