From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 pretyping/unification.mli | 77 ++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 60 insertions(+), 17 deletions(-)

(limited to 'pretyping/unification.mli')

diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 75bddc1f..119b1a75 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,34 +10,43 @@ open Term
 open Environ
 open Evd
 
-type unify_flags = {
+type core_unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly_in_conv_on_closed_terms : bool;
+  use_evars_eagerly_in_conv_on_closed_terms : bool;
   modulo_delta : Names.transparent_state;
   modulo_delta_types : Names.transparent_state;
-  modulo_delta_in_merge : Names.transparent_state option;
   check_applied_meta_types : bool;
-  resolve_evars : bool;
   use_pattern_unification : bool;
   use_meta_bound_pattern_unification : bool;
-  frozen_evars : ExistentialSet.t;
+  frozen_evars : Evar.Set.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
+type unify_flags = {
+  core_unify_flags : core_unify_flags;
+  merge_unify_flags : core_unify_flags;
+  subterm_unify_flags : core_unify_flags;
+  allow_K_in_toplevel_higher_order_unification : bool;
+  resolve_evars : bool
+}
+
+val default_core_unify_flags : unit -> core_unify_flags
+val default_no_delta_core_unify_flags : unit -> core_unify_flags
+
+val default_unify_flags : unit -> unify_flags
+val default_no_delta_unify_flags : unit -> unify_flags
 
-val elim_flags : unify_flags
-val elim_no_delta_flags : unify_flags
+val elim_flags : unit -> unify_flags
+val elim_no_delta_flags : unit -> unify_flags
 
 (** The "unique" unification fonction *)
 val w_unify :
   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 m (c,t)] 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 :
@@ -53,25 +62,59 @@ val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map
 val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
   evar_map * constr
 
+(* Looking for subterms in contexts at some occurrences, possibly with pattern*)
+
+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
+| AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
+
+val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
+  env -> Evd.evar_map -> pending_constr -> Evd.evar_map * constr
+
+type abstraction_result =
+  Names.Id.t * named_context_val *
+    Context.named_declaration list * Names.Id.t option *
+    types * (Evd.evar_map * constr) option
+
+val make_abstraction : env -> Evd.evar_map -> constr ->
+  abstraction_request -> abstraction_result
+
+val pose_all_metas_as_evars : env -> evar_map -> constr -> 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 
+(** [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
-
+  env -> evar_map -> constr -> constr -> constr list -> evar_map * (constr * types)
 
 (* For tracing *)
 
-val w_merge : env -> bool -> unify_flags -> evar_map *
+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
 
 val unify_0 :            Environ.env ->
            Evd.evar_map ->
            Evd.conv_pb ->
-           unify_flags ->
+           core_unify_flags ->
+           Term.types ->
+           Term.types ->
+           Evd.evar_map * Evd.metabinding list *
+           (Environ.env * Term.types Term.pexistential * Term.constr) list
+
+val unify_0_with_initial_metas : 
+           Evd.evar_map * Evd.metabinding list *
+           (Environ.env * Term.types Term.pexistential * Term.constr) list ->
+           bool ->
+           Environ.env ->
+           Evd.conv_pb ->
+           core_unify_flags ->
            Term.types ->
            Term.types ->
            Evd.evar_map * Evd.metabinding list *
-- 
cgit v1.2.3