diff options
| author | Pierre Letouzey | 2017-05-11 16:12:12 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-05-22 15:15:49 +0200 |
| commit | f3b186bad386f6215aa9d9ebd02ab97246ee50c1 (patch) | |
| tree | b6cbdeae201230ebc041b7ac716c248695d78133 /kernel/type_errors.ml | |
| parent | 2c01ce4b5d52a9f86553d07a83a237902b0cbc64 (diff) | |
romega: shorter trace (no more term lengths)
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions