Include review suggestions

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;