diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 3396c5a0e7..8be7b1477b 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -45,6 +45,13 @@ type typing_constraint = | WithoutTypeConstraint (** A term of unknown expected type *) type use_typeclasses = NoUseTC | UseTCForConv | UseTC +(** Typeclasses are used in 2 ways: + +- through the "Typeclass Resolution For Conversion" option, if a + conversion problem fails we try again after resolving typeclasses + (UseTCForConv and UseTC) +- after pretyping we resolve typeclasses (UseTC) (in [solve_remaining_evars]) +*) type inference_flags = { use_typeclasses : use_typeclasses; |