diff options
| author | Hugo Herbelin | 2019-11-14 12:50:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-01-30 18:59:26 +0100 |
| commit | a086919e4bab3fba4469d7374851a2d95021f528 (patch) | |
| tree | 59972639ab26a2291cd63d951306a9b5fa3c760f /kernel/type_errors.ml | |
| parent | a71fa32802d05bfe63263730c40e93015bb71f8b (diff) | |
Minor indentation change.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions