diff options
| author | Hugo Herbelin | 2015-12-10 09:25:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:20 +0100 |
| commit | 006e1a5bf9e90fba3ba9fa1541e7ed8978c99441 (patch) | |
| tree | 1d22ff77bd1ee11502a9c4325f3dee7c473f22e6 /kernel/type_errors.ml | |
| parent | 9e12f35ddf03dd47af99284fa9bfbb14759834b8 (diff) | |
Refman, ch. 4: A few fixes.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions