diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-09 18:05:33 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-09 18:05:33 +0000 |
commit | 38f734040d5fad0f5170a1fdee6f96e3e4f1c06d (patch) | |
tree | 67e815b64a118233e2eeba4ec64dafa47a874782 | |
parent | bd4034520da83bc667161c0e397b3720d3884b2f (diff) |
A few comments in evarconv.mli.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16498 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | pretyping/evarconv.mli | 36 |
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 +(**/**) |