diff options
| author | Matthieu Sozeau | 2019-07-23 17:46:02 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-08-26 16:21:44 +0200 |
| commit | 1e434fe4421bee0b1928fd015fb60025ec6c2833 (patch) | |
| tree | daf05873483935b52df35127ff1da816a7a2e709 /kernel/type_errors.ml | |
| parent | eb3f8225a286aef3a57ad876584b4a927241ff69 (diff) | |
Document `Template Check` flag and add changelog entry for 9918
Fix changelog entry
Fix build of the user manual
Markup fixes from Théo Zimmermann
Update doc and changelog and improve error messages.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions