Documenting a bit more interpretation functions in passing.

1 files changed, 17 insertions, 7 deletions

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index a6aa08657..5f0e19cf2 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -66,9 +66,12 @@ val all_and_fail_flags : inference_flags
 (** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
-(** Generic call to the interpreter from glob_constr to open_constr, leaving
-    unresolved holes as evars and returning the typing contexts of
-    these evars. Work as [understand_gen] for the rest. *)
+(** Generic calls to the interpreter from glob_constr to open_constr;
+    by default, inference_flags tell to use type classes and
+    heuristics (but no external tactic solver hooks), as well as to
+    ensure that conversion problems are all solved and expand evars,
+    but unresolved evars can remain. The difference is in whether the
+    evar_map is modified explicitly or by side-effect. *)
 
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> open_constr
@@ -92,7 +95,12 @@ val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
   typing_constraint -> glob_constr -> pure_open_constr
 
-(** Standard call to get a constr from a glob_constr, resolving implicit args *)
+(** Standard call to get a constr from a glob_constr, resolving
+    implicit arguments and coercions, and compiling pattern-matching;
+    the default inference_flags tells to use type classes and
+    heuristics (but no external tactic solver hook), as well as to
+    ensure that conversion problems are all solved and that no
+    unresolved evar remains, expanding evars. *)
 
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
   env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
@@ -102,12 +110,13 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
 val understand_judgment : env -> evar_map -> 
   glob_constr -> unsafe_judgment Evd.in_evar_universe_context
 
-(** Idem but do not fail on unresolved evars *)
+(** Idem but do not fail on unresolved evars (type cl*)
 val understand_judgment_tcc : env -> evar_map ref ->
   glob_constr -> unsafe_judgment
 
 (** Trying to solve remaining evars and remaining conversion problems
-    with type classes, heuristics, and possibly an external solver *)
+    possibly using type classes, heuristics, external tactic solver
+    hook depending on given flags. *)
 (* For simplicity, it is assumed that current map has no other evars
    with candidate and no other conversion problems that the one in
    [pending], however, it can contain more evars than the pending ones. *)
@@ -115,7 +124,8 @@ val understand_judgment_tcc : env -> evar_map ref ->
 val solve_remaining_evars : inference_flags ->
   env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map
 
-(** Checking evars are all solved and reporting an appropriate error message *)
+(** Checking evars and pending conversion problems are all solved,
+    reporting an appropriate error message *)
 
 val check_evars_are_solved :
   env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit