diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-10 22:00:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-10 22:00:04 +0000 |
| commit | d74f1da437c214cc0c960e87e8bbf04dd214128e (patch) | |
| tree | 017dc70a7db4dc08a1f414aeacec631a47bc91ad /pretyping/evarutil.mli | |
| parent | 32bcb10ce3470377314b964223ce9aed1ab33c72 (diff) | |
Passed conv_algo to evar_define and move call to solve_refl to
evar_define so that it can recursively deal with evar/evar problems.
Also, check_evar_instance now called after each instantiation.
Also did a bit of file reformatting.
The commit apparently induces a loss of some 0,4% on the compilation
of the standard library. Maybe, introducing a heuristic to decide when
to call check_evar_instance (which I guess is responsible for the
overhead) might be a good thing to look at?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index acf92915e..7c06d41c9 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -52,11 +52,15 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list (** {6 Instantiate evars} *) +type conv_fun = + env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool + (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev] *) -val evar_define : ?choose:bool -> env -> existential -> constr -> evar_map -> evar_map +val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> + existential -> constr -> evar_map (** {6 Evars/Metas switching...} *) @@ -78,14 +82,11 @@ val whd_head_evar : evar_map -> constr -> constr val is_ground_term : evar_map -> constr -> bool val is_ground_env : evar_map -> env -> bool -val solve_refl : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) - -> env -> evar_map -> existential_key -> constr array -> constr array -> - evar_map -val solve_simple_eqn : - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) - -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> - evar_map * bool +val solve_refl : conv_fun -> env -> evar_map -> + existential_key -> constr array -> constr array -> evar_map +val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> + bool option * existential * constr -> evar_map * bool +val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) @@ -202,6 +203,6 @@ val push_rel_context_to_named_context : Environ.env -> types -> val generalize_evar_over_rels : evar_map -> existential -> types * constr list -val check_evar_instance : evar_map -> existential_key -> - (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) -> evar_map +val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun -> + evar_map |