diff options
| author | Matthieu Sozeau | 2016-11-07 14:50:56 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-07 14:50:56 +0100 |
| commit | 25a60b1fcfa2f6017bedd986b1f90fe923d0f3ad (patch) | |
| tree | a67e7204fc6d311da6eb39d9c7c25f8de7cd8764 /kernel/type_errors.ml | |
| parent | 1f36cdefd841526f804bd2dd51c1d88309333376 (diff) | |
Document two new variants of refine
They allow to call refine without doing typeclass resolution, allowing
to use refine in typeclass hints.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions