diff options
| author | Matthieu Sozeau | 2015-01-13 07:09:05 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-13 07:09:05 +0530 |
| commit | 74682bb27da074fedc115238f3085baaccf12d73 (patch) | |
| tree | 3d8a70616ae17fe27e960fc38bf1c9d799131e87 /kernel/nativelib.ml | |
| parent | 9993ac283e14c0f789b9fa826fd20086059cdcd8 (diff) | |
TCs: Properly handle Hint Extern with conclusions of the form _ -> _
in typeclasses eauto, remaining compatible with eauto and still
producing eta-reduced applications for Hint Resolves. Fixes bug #3794.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions