diff options
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 56 |
1 files changed, 40 insertions, 16 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 2f48081a..e4bca4d3 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,54 +1,78 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: unification.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Term open Environ open Evd -(*i*) type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; - use_metas_eagerly : bool; + use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; + modulo_delta_types : Names.transparent_state; + check_applied_meta_types : bool; resolve_evars : bool; - use_evars_pattern_unification : bool + use_pattern_unification : bool; + use_meta_bound_pattern_unification : bool; + frozen_evars : ExistentialSet.t; + restrict_conv_on_strict_subterms : bool; + modulo_betaiota : bool; + modulo_eta : bool; + allow_K_in_toplevel_higher_order_unification : bool } val default_unify_flags : unify_flags val default_no_delta_unify_flags : unify_flags -(* The "unique" unification fonction *) +val elim_flags : unify_flags +val elim_no_delta_flags : unify_flags + +(** The "unique" unification fonction *) val w_unify : - bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map + env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -(* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a +(** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a subterm of [t]. Constraints are added to [m] and the matched subterm of [t] is also returned. *) val w_unify_to_subterm : - env -> ?flags:unify_flags -> constr * constr -> evar_map -> evar_map * constr + env -> evar_map -> ?flags:unify_flags -> constr * constr -> evar_map * constr val w_unify_to_subterm_all : - env -> ?flags:unify_flags -> constr * constr -> evar_map -> (evar_map * constr) list + env -> evar_map -> ?flags:unify_flags -> constr * constr -> (evar_map * constr) list val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map -(* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type +(** [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type [ctyp] so that its gets type [typ]; [typ] may contain metavariables *) val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> evar_map * constr (*i This should be in another module i*) -(* [abstract_list_all env evd t c l] *) -(* abstracts the terms in l over c to get a term of type t *) -(* (exported for inv.ml) *) +(** [abstract_list_all env evd t c l] + abstracts the terms in l over c to get a term of type t + (exported for inv.ml) *) val abstract_list_all : env -> evar_map -> constr -> constr -> constr list -> constr + + +(* For tracing *) + +val w_merge : env -> bool -> unify_flags -> evar_map * + (metavariable * constr * (instance_constraint * instance_typing_status)) list * + (env * types pexistential * types) list -> evar_map + +val unify_0 : Environ.env -> + Evd.evar_map -> + Evd.conv_pb -> + unify_flags -> + Term.types -> + Term.types -> + Evd.evar_map * Evd.metabinding list * + (Environ.env * Term.types Term.pexistential * Term.constr) list + |