summaryrefslogtreecommitdiff
path: root/pretyping/unification.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/unification.mli')
-rw-r--r--pretyping/unification.mli56
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
+