A few comments in evarconv.mli.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16498 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 10 deletions

diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9d0c79143..655dc1c1a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -15,8 +15,12 @@ open Reductionops
 open Evd
 open Locus
 
+(** Unification for type inference. } *)
+
 exception UnableToUnify of evar_map * Pretype_errors.unification_error
 
+(** {6 Main unification algorithm for type inference. } *)
+
 (** returns exception NotUnifiable with best known evar_map if not unifiable *)
 val the_conv_x     : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
 val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
@@ -26,25 +30,37 @@ val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_ma
 val e_conv  : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool
 val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool
 
-(**/**)
-(* For debugging *)
-val evar_conv_x : transparent_state ->
-  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
-val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state ->
-  env -> evar_map ->
-    conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
-      Evarsolve.unification_result
-(**/**)
+(** {6 Unification heuristics. } *)
+
+(** Try heuristics to solve pending unification problems and to solve
+    evars with candidates *)
 
 val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
 
+(** Check if a canonical structure is applicable *)
+
 val check_conv_record : constr * types stack -> constr * types stack ->
   constr * constr list * (constr list * constr list) *
     (constr list * types list) *
     (constr stack * types stack) * constr *
     (int * constr)
 
-val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
+(** Try to solve problems of the form ?x[args] = c by second-order
+    matching, using typing to select occurrences *)
 
 val second_order_matching : transparent_state -> env -> evar_map ->
   existential -> occurrences option list -> constr -> evar_map * bool
+
+(** Declare function to enforce evars resolution by using typing constraints *)
+
+val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
+
+(**/**)
+(* For debugging *)
+val evar_conv_x : transparent_state ->
+  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
+val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state ->
+  env -> evar_map ->
+    conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
+      Evarsolve.unification_result
+(**/**)