diff options
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0ad882a9..16ce5c93 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,12 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open Constr +open EConstr open Environ open Evd @@ -44,7 +47,7 @@ val elim_no_delta_flags : unit -> unify_flags val is_keyed_unification : unit -> bool -(** The "unique" unification fonction *) +(** The "unique" unification function *) val w_unify : env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map @@ -71,18 +74,18 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma + env -> evar_map -> (evar_map * constr) -> evar_map * constr type 'r abstraction_result = Names.Id.t * named_context_val * - Context.Named.Declaration.t list * Names.Id.t option * - types * (constr, 'r) Sigma.sigma option + named_declaration list * Names.Id.t option * + types * (evar_map * constr) option -val make_abstraction : env -> 'r Sigma.t -> constr -> +val make_abstraction : env -> evar_map -> constr -> abstraction_request -> 'r abstraction_result val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr @@ -97,28 +100,29 @@ val abstract_list_all : (* For tracing *) -val w_merge : env -> bool -> core_unify_flags -> evar_map * - (metavariable * constr * (instance_constraint * instance_typing_status)) list * - (env * types pexistential * types) list -> evar_map +type metabinding = (metavariable * constr * (instance_constraint * instance_typing_status)) + +type subst0 = + (evar_map * + metabinding list * + (Environ.env * existential * t) list) + +val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map val unify_0 : Environ.env -> Evd.evar_map -> Evd.conv_pb -> core_unify_flags -> - Term.types -> - Term.types -> - Evd.evar_map * Evd.metabinding list * - (Environ.env * Term.types Term.pexistential * Term.constr) list + types -> + types -> + subst0 val unify_0_with_initial_metas : - Evd.evar_map * Evd.metabinding list * - (Environ.env * Term.types Term.pexistential * Term.constr) list -> + subst0 -> bool -> Environ.env -> Evd.conv_pb -> core_unify_flags -> - Term.types -> - Term.types -> - Evd.evar_map * Evd.metabinding list * - (Environ.env * Term.types Term.pexistential * Term.constr) list - + types -> + types -> + subst0 |