diff options
| author | Théo Zimmermann | 2019-05-22 21:11:06 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-23 16:35:16 +0200 |
| commit | b83b6dc0aca0a7a9150d49ef3a6e968a7e5433f6 (patch) | |
| tree | 0179184428304d3363f882d2cf31a845731b79aa /kernel/type_errors.ml | |
| parent | e7628797fc241a4d7a5c1a5675cb679db282050d (diff) | |
Define many undefined tokens, and other misc fixes.
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions