diff options
| author | Pierre-Marie Pédrot | 2015-09-21 15:54:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-09-21 15:54:19 +0200 |
| commit | 7c5356ed487dcf7cf915e5471832852f7002586c (patch) | |
| tree | 27fb39d29bf25dca6bc24cc4a1f088dbaeaec82c /kernel/type_errors.ml | |
| parent | 0ac3a2f4de0dc02b973c9f5d59b3c0a97f888141 (diff) | |
Fixing tutorial.
The V7 to V8 translator lost part of term annotations.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions