From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 pretyping/unification.mli | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

(limited to 'pretyping/unification.mli')

diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 6be530be..89280631 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: unification.mli 6142 2004-09-27 19:33:01Z sacerdot $ i*)
+(*i $Id: unification.mli 10856 2008-04-27 16:15:34Z herbelin $ i*)
 
 (*i*)
 open Term
@@ -14,20 +14,36 @@ open Environ
 open Evd
 (*i*)
 
+type unify_flags = { 
+  modulo_conv_on_closed_terms : Names.transparent_state option; 
+  use_metas_eagerly : bool;
+  modulo_delta : Names.transparent_state;
+}
+
+val default_unify_flags : unify_flags
+val default_no_delta_unify_flags : unify_flags
+
 (* The "unique" unification fonction *)
 val w_unify :
-  bool -> env -> conv_pb -> ?mod_delta:bool -> constr -> constr -> evar_defs -> evar_defs
+  bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_defs -> evar_defs
 
 (* [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 -> ?mod_delta:bool -> constr * constr -> evar_defs -> evar_defs * constr
+  env -> ?flags:unify_flags -> constr * constr -> evar_defs -> evar_defs * constr
+
+val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs
+
+(* [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_defs -> constr -> types -> types ->
+  evar_defs * constr
 
 (*i This should be in another module i*)
 
-(* [abstract_list_all env sigma t c l]                     *)
+(* [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_defs -> constr -> constr -> constr list -> constr
-- 
cgit v1.2.3