From fafc731885f84656ec884d40b843aa62a5991025 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Mar 2020 13:34:17 +0200
Subject: Include review suggestions

---
 pretyping/pretyping.mli | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'pretyping')

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;
-- 
cgit v1.2.3