Documenting a bit more interpretation functions in passing.

2 files changed, 22 insertions, 10 deletions

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4d2c994679..b671c98815 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -95,7 +95,8 @@ val intern_context : bool -> env -> internalization_env -> local_binder list ->
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
-(** Main interpretation functions expecting evars to be all resolved *)
+(** Main interpretation functions, using type class inference,
+    expecting evars and pending problems to be all resolved *)
 
 val interp_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> constr Evd.in_evar_universe_context
@@ -106,9 +107,10 @@ val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
 val interp_type : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types Evd.in_evar_universe_context
 
-(** Main interpretation function expecting evars to be all resolved *)
+(** Main interpretation function expecting all postponed problems to
+    be resolved, but possibly leaving evars. *)
 
-val interp_open_constr   : env -> evar_map -> constr_expr -> evar_map * constr
+val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
 
 (** Accepting unresolved evars *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index a6aa086579..5f0e19cf2b 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