diff options
| author | Maxime Dénès | 2016-11-07 15:46:24 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-07 15:46:24 +0100 |
| commit | b58f5b2b499b687288587837cbf0cfc04a269c75 (patch) | |
| tree | c4186f582884cc7b295eccc163ca893c53009fb6 /kernel/type_errors.ml | |
| parent | 6f30019bfd99a0125fdc12baf8b6c04169701fb7 (diff) | |
| parent | d7cb0e2115ec37eddeeecbb1f2dbdeb7e49aeb7a (diff) | |
Merge remote-tracking branch 'github/pr/339' into v8.6
Was PR#339: Documenting type class options, typeclasses eauto
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions