Imported Upstream version 8.4~betaupstream/8.4_beta

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
+