diff options
| author | Hugo Herbelin | 2020-04-13 20:01:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-05 19:09:07 +0100 |
| commit | cb105b62f597b2a51fad743547647e4885d6365a (patch) | |
| tree | 3bafd03e6e9413014a4bd5af39dc028fb65c8a9d /kernel/type_errors.mli | |
| parent | d276a494d29ea69c6a60b16da5dddb9d39f287ca (diff) | |
Notations: Giving a consistent role to global references occurring patterns.
Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.
We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.
Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions