diff options
| author | Maxime Dénès | 2016-12-02 15:52:46 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-12-02 15:52:46 +0100 |
| commit | fa1e627e12831417694b4fb538154721111741b5 (patch) | |
| tree | 48a6e637aa6a4f558fa48e93ef59b5fea44cf270 /kernel/type_errors.mli | |
| parent | 0ea7bdc2e315da9a0a8338e5099dfcaad0bac9ef (diff) | |
| parent | 910a1aec499b304006f2a9291811087ca3c4c7a1 (diff) | |
Merge remote-tracking branch 'github/pr/381' into v8.6
Was PR#381: V8.6+fix typeclasses eauto shelving
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions