premiere reorganisation de l\'unification

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 861 insertions, 176 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 3f9dc5c887..ceb23cc782 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -13,7 +13,6 @@ open Pp
 open Term
 open Names
 open Environ
-open Instantiate
 open Univ
 open Evd
 open Closure
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 33ad61213a..3ca777647d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -13,7 +13,6 @@ open Names
 open Term
 open Reductionops
 open Closure
-open Instantiate
 open Environ
 open Typing
 open Classops
@@ -66,7 +65,7 @@ let evar_apprec_nobeta env isevars stack c =
     let (t,stack as s') = apprec_nobeta env (evars_of isevars) s in
     match kind_of_term t with
       | Evar (n,_ as ev) when Evd.is_defined (evars_of isevars) n ->
-	  aux (existential_value (evars_of isevars) ev, stack)
+	  aux (Evd.existential_value (evars_of isevars) ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 *)
@@ -77,7 +76,7 @@ let evar_apprec env isevars stack c =
     let (t,stack as s') = Reductionops.apprec env sigma s in
     match kind_of_term t with
       | Evar (n,_ as ev) when Evd.is_defined sigma n ->
-	  aux (existential_value sigma ev, stack)
+	  aux (Evd.existential_value sigma ev, stack)
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 97681f9183..f5b8c6288d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -18,7 +18,6 @@ open Termops
 open Sign
 open Environ
 open Evd
-open Instantiate
 open Reductionops
 open Indrec
 open Pretype_errors
@@ -593,3 +592,34 @@ let split_tycon loc env isevars = function
 let valcon_of_tycon x = x
 
 let lift_tycon = option_app (lift 1)
+
+(*************************************)
+(* Metas *)
+
+let meta_val_of env mv = 
+  let rec valrec mv =
+    try
+      (match Metamap.find mv env with
+	 | Cltyp _ -> mkMeta mv
+	 | Clval(b,_) ->
+	     instance (List.map (fun mv' -> (mv',valrec mv')) 
+			       (Metaset.elements b.freemetas)) b.rebus)
+    with Not_found -> 
+      mkMeta mv
+  in 
+  valrec mv
+
+let meta_instance env b =
+  let c_sigma =
+    List.map 
+      (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas)
+  in 
+  instance c_sigma b.rebus
+
+let nf_meta env c = meta_instance env (mk_freelisted c)
+
+let meta_type env mv =
+  let ty =
+    try meta_ftype env mv
+    with Not_found -> error ("unknown meta ?"^string_of_int mv) in
+  meta_instance env ty
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 29331aa5e1..a08fb3f822 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -100,3 +100,8 @@ val split_tycon :
 val valcon_of_tycon : type_constraint -> val_constraint
 
 val lift_tycon : type_constraint -> type_constraint
+
+(* Metas *)
+val nf_meta       : meta_map -> constr -> constr
+val meta_type     : meta_map -> metavariable -> types
+val meta_instance : meta_map -> constr freelisted -> constr
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d775f9fe93..be35cb9475 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Term
 open Sign
+open Environ
 
 (* The type of mappings for existential variables *)
 
@@ -63,3 +64,142 @@ let evar_body ev = ev.evar_body
 let string_of_existential ev = "?" ^ string_of_int ev
 
 let existential_of_int ev = ev
+
+(*******************************************************************)
+(* Formerly Instantiate module *)
+
+let is_id_inst inst =
+  let is_id (id,c) = match kind_of_term c with
+    | Var id' -> id = id'
+    | _ -> false
+  in
+  List.for_all is_id inst
+
+(* Vérifier que les instances des let-in sont compatibles ?? *)
+let instantiate_sign_including_let sign args =
+  let rec instrec = function
+    | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
+    | ([],[])                        -> []
+    | ([],_) | (_,[]) ->
+    anomaly "Signature and its instance do not match"
+  in 
+  instrec (sign,args)
+
+let instantiate_evar sign c args =
+  let inst = instantiate_sign_including_let sign args in
+  if is_id_inst inst then
+    c
+  else
+    replace_vars inst c
+
+(* Existentials. *)
+
+let existential_type sigma (n,args) =
+  let info =
+    try map sigma n
+    with Not_found ->
+      anomaly ("Evar "^(string_of_existential n)^" was not declared") in
+  let hyps = info.evar_hyps in
+  instantiate_evar hyps info.evar_concl (Array.to_list args)
+
+exception NotInstantiatedEvar
+
+let existential_value sigma (n,args) =
+  let info = map sigma n in
+  let hyps = info.evar_hyps in
+  match evar_body info with
+    | Evar_defined c ->
+	instantiate_evar hyps c (Array.to_list args)
+    | Evar_empty ->
+	raise NotInstantiatedEvar
+
+let existential_opt_value sigma ev =
+  try Some (existential_value sigma ev)
+  with NotInstantiatedEvar -> None
+
+(*******************************************************************)
+(* The type constructor ['a sigma] adds an evar map to an object of
+  type ['a] *)
+type 'a sigma = {
+  it : 'a ;
+  sigma : evar_map}
+ 
+let sig_it x = x.it
+let sig_sig x = x.sigma
+ 
+(*******************************************************************)
+(* Metamaps *)
+
+(*******************************************************************)
+(*            Constraints for existential variables                *)
+(*******************************************************************)
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Intset.t }
+
+(* Collects all metavars appearing in a constr *)
+let metavars_of c =
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Meta mv -> Intset.add mv acc
+      | _         -> fold_constr collrec acc c
+  in
+  collrec Intset.empty c
+
+let mk_freelisted c =
+  { rebus = c; freemetas = metavars_of c }
+
+
+(* Clausal environments *)
+
+type clbinding =
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+let map_fl f cfl = { cfl with rebus=f cfl.rebus }
+
+let map_clb f = function
+  | Cltyp cfl -> Cltyp (map_fl f cfl)
+  | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2)
+
+(***********************)
+                                                                               
+module Metaset = Intset
+                                                                               
+let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false
+
+module Metamap = Intmap
+
+let metamap_in_dom x m =
+  try let _ = Metamap.find x m in true with Not_found -> false
+
+                                                                               
+let metamap_to_list m =
+  Metamap.fold (fun n v l -> (n,v)::l) m []
+ 
+let metamap_inv m b =
+  Metamap.fold (fun n v l -> if v = b then n::l else l) m []
+ 
+type meta_map = clbinding Metamap.t
+ 
+let meta_defined env mv =
+  match Metamap.find mv env with
+    | Clval _ -> true
+    | Cltyp _ -> false
+ 
+let meta_fvalue env mv =
+  match Metamap.find mv env with
+    | Clval(b,_) -> b
+    | Cltyp _ -> anomaly "meta_fvalue: meta has no value"
+           
+let meta_ftype env mv =
+  match Metamap.find mv env with
+    | Cltyp b -> b
+    | Clval(_,b) -> b
+ 
+let meta_declare mv v menv =
+  Metamap.add mv (Cltyp(mk_freelisted v)) menv
+  
+let meta_assign mv v menv =
+  Metamap.add mv (Clval(mk_freelisted v, meta_ftype menv mv)) menv
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 567097d0d5..3f9eaa5fa7 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -54,3 +54,54 @@ val evar_body : evar_info -> evar_body
 
 val string_of_existential : evar -> string
 val existential_of_int : int -> evar
+
+(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+    no body and [Not_found] if it does not exist in [sigma] *)
+
+exception NotInstantiatedEvar
+val existential_value : evar_map -> existential -> constr
+val existential_type : evar_map -> existential -> types
+val existential_opt_value : evar_map -> existential -> constr option
+
+(*************************)
+(* The type constructor ['a sigma] adds an evar map to an object of
+  type ['a] *)
+type 'a sigma = {
+  it : 'a ;
+  sigma : evar_map}
+
+val sig_it  : 'a sigma -> 'a
+val sig_sig : 'a sigma -> evar_map
+
+(*************************)
+(* Meta map *)
+
+module Metaset : Set.S with type elt = metavariable
+
+val meta_exists : (metavariable -> bool) -> Metaset.t -> bool
+
+module Metamap : Map.S with type key = metavariable
+
+val metamap_in_dom : metavariable -> 'a Metamap.t -> bool
+val metamap_to_list : 'a Metamap.t -> (metavariable * 'a) list
+val metamap_inv : 'a Metamap.t -> 'a -> metavariable list
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Metaset.t }
+
+val mk_freelisted : constr -> constr freelisted
+val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
+
+type clbinding =
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+val map_clb : (constr -> constr) -> clbinding -> clbinding
+
+type meta_map = clbinding Metamap.t
+val meta_defined : meta_map -> metavariable -> bool
+val meta_fvalue   : meta_map -> metavariable -> constr freelisted
+val meta_ftype    : meta_map -> metavariable -> constr freelisted
+val meta_declare : metavariable -> types -> meta_map -> meta_map
+val meta_assign  : metavariable -> constr -> meta_map -> meta_map
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8d1917d76f..11cb50c83a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -19,7 +19,6 @@ open Declarations
 open Entries
 open Inductive
 open Inductiveops
-open Instantiate
 open Environ
 open Reductionops
 open Typeops
diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml
deleted file mode 100644
index fd9ed1995d..0000000000
--- a/pretyping/instantiate.ml
+++ /dev/null
@@ -1,68 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Sign
-open Evd
-open Declarations
-open Environ
-
-let is_id_inst inst =
-  let is_id (id,c) = match kind_of_term c with
-    | Var id' -> id = id'
-    | _ -> false
-  in
-  List.for_all is_id inst
-
-(* Vérifier que les instances des let-in sont compatibles ?? *)
-let instantiate_sign_including_let sign args =
-  let rec instrec = function
-    | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
-    | ([],[])                        -> []
-    | ([],_) | (_,[]) ->
-    anomaly "Signature and its instance do not match"
-  in 
-  instrec (sign,args)
-
-let instantiate_evar sign c args =
-  let inst = instantiate_sign_including_let sign args in
-  if is_id_inst inst then
-    c
-  else
-    replace_vars inst c
-
-(* Existentials. *)
-
-let existential_type sigma (n,args) =
-  let info =
-    try Evd.map sigma n
-    with Not_found ->
-      anomaly ("Evar "^(string_of_existential n)^" was not declared") in
-  let hyps = info.evar_hyps in
-  instantiate_evar hyps info.evar_concl (Array.to_list args)
-
-exception NotInstantiatedEvar
-
-let existential_value sigma (n,args) =
-  let info = Evd.map sigma n in
-  let hyps = info.evar_hyps in
-  match evar_body info with
-    | Evar_defined c ->
-	instantiate_evar hyps c (Array.to_list args)
-    | Evar_empty ->
-	raise NotInstantiatedEvar
-
-let existential_opt_value sigma ev =
-  try Some (existential_value sigma ev)
-  with NotInstantiatedEvar -> None
-
diff --git a/pretyping/instantiate.mli b/pretyping/instantiate.mli
deleted file mode 100644
index 6de2582967..0000000000
--- a/pretyping/instantiate.mli
+++ /dev/null
@@ -1,25 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Names
-open Term
-open Evd
-open Sign
-open Environ
-(*i*)
-
-(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
-no body and [Not_found] if it does not exist in [sigma] *)
-
-exception NotInstantiatedEvar
-val existential_value : evar_map -> existential -> constr
-val existential_type : evar_map -> existential -> types
-val existential_opt_value : evar_map -> existential -> constr option
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 07d72c89e1..d7407c5d1d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -26,6 +26,9 @@ type pretype_error =
   | OccurCheck of existential_key * constr
   | NotClean of existential_key * constr * hole_kind
   | UnsolvableImplicit of hole_kind
+  | CannotUnify of constr * constr
+  | CannotGeneralize of constr
+  | NoOccurrenceFound of constr
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -33,6 +36,12 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
+let precatchable_exception = function
+  | Util.UserError _ | TypeError _ | PretypeError _
+  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
+    Nametab.GlobalizationError _ | PretypeError _)) -> true
+  | _ -> false
+
 let nf_evar = Reductionops.nf_evar
 let j_nf_evar sigma j = 
   { uj_val = nf_evar sigma j.uj_val;
@@ -141,6 +150,9 @@ let error_not_clean env sigma ev c (loc,k) =
 let error_unsolvable_implicit loc env sigma e =
   raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit e))
 
+let error_cannot_unify env sigma (m,n) =
+  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e09a6d1d10..2f9b1dc46a 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -28,6 +28,9 @@ type pretype_error =
   | OccurCheck of existential_key * constr
   | NotClean of existential_key * constr * hole_kind
   | UnsolvableImplicit of hole_kind
+  | CannotUnify of constr * constr
+  | CannotGeneralize of constr
+  | NoOccurrenceFound of constr
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -35,6 +38,8 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
+val precatchable_exception : exn -> bool
+
 (* Presenting terms without solved evars *)
 val nf_evar :  Evd.evar_map -> constr -> constr
 val j_nf_evar :  Evd.evar_map -> unsafe_judgment -> unsafe_judgment
@@ -82,6 +87,8 @@ val error_not_clean :
 
 val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b
 
+val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
+
 (*s Ml Case errors *)
 
 val error_cant_find_case_type_loc :
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 36247edc7f..dcb30c4d00 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -37,7 +37,6 @@ open Dyn
 open Declarations
 open Inductive
 open Inductiveops
-open Instantiate
 
 let lift_context n l = 
   let k = List.length l in 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index c7a0dfe7a9..a9fc90df26 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -17,7 +17,6 @@ open Univ
 open Evd
 open Declarations
 open Environ
-open Instantiate
 open Closure
 open Esubst
 open Reduction
@@ -428,7 +427,7 @@ let whd_betadeltaiota_nolet env sigma x =
 let rec whd_evar sigma c =
   match kind_of_term c with
     | Evar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
-	whd_evar sigma (Instantiate.existential_value sigma (ev,args))
+	whd_evar sigma (Evd.existential_value sigma (ev,args))
     | _ -> collapse_appl c
 
 let nf_evar sigma =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 6d2ff5d03b..5a71b28d8d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -16,7 +16,6 @@ open Reductionops
 open Environ
 open Typeops
 open Declarations
-open Instantiate
 
 let outsort env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
@@ -61,7 +60,7 @@ let typeur sigma metamap =
     | Const c ->
         let cb = lookup_constant c env in
         body_of_type cb.const_type
-    | Evar ev -> existential_type sigma ev
+    | Evar ev -> Evd.existential_type sigma ev
     | Ind ind -> body_of_type (type_of_inductive env ind)
     | Construct cstr -> body_of_type (type_of_constructor env cstr)
     | Case (_,p,c,lf) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7af108a4ef..9059c105f6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -20,7 +20,6 @@ open Inductive
 open Environ
 open Reductionops
 open Closure
-open Instantiate
 open Cbv
 open Rawterm
 
@@ -94,7 +93,7 @@ let reference_opt_value sigma env = function
   | EvalRel n ->
       let (_,v,_) = lookup_rel n env in
       option_app (lift n) v
-  | EvalEvar ev -> existential_opt_value sigma ev
+  | EvalEvar ev -> Evd.existential_opt_value sigma ev
 
 exception NotEvaluable
 let reference_value sigma env c =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 7c4739b489..02e8618dc5 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -89,6 +89,9 @@ let rec print_constr c = match kind_of_term c with
            cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++
          str"}")
 
+let term_printer = ref print_constr
+let set_print_constr f = term_printer := f
+
 (*let current_module = ref empty_dirpath
 
 let set_module m = current_module := m*)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 255e8a056b..8ce7b39dcb 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -20,10 +20,14 @@ open Environ
 val new_univ : unit -> Univ.universe
 val new_sort_in_family : sorts_family -> sorts
 
-(* iterators on terms *)
+(* printers *)
 val print_sort : sorts -> std_ppcmds
 val print_sort_family : sorts_family -> std_ppcmds
+(* debug printer: do not use to display terms to the casual user... *)
 val print_constr : constr -> std_ppcmds
+val set_print_constr : (constr -> std_ppcmds) -> unit
+
+(* iterators on terms *)
 val prod_it : init:types -> (name * types) list -> types
 val lam_it : init:constr -> (name * types) list -> constr
 val rel_vect : int -> int -> constr array
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 844652fd86..b98ff0e7dc 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -21,29 +21,29 @@ open Typeops
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
-type 'a mach_flags = {
-  fix : bool;
-  nocheck : bool }
-
 (* The typing machine without information, without universes but with
    existential variables. *)
 
-let assumption_of_judgment env sigma j =
+let assumption_of_judgment env (sigma,_) j =
   assumption_of_judgment env (j_nf_evar sigma j)
 
-let type_judgment env sigma j =
+let type_judgment env (sigma,_) j =
   type_judgment env (j_nf_evar sigma j)
 
+let check_type env (sigma,_) j ty =
+  if not (is_conv_leq env sigma j.uj_type ty) then
+    error_actual_type env (j_nf_evar sigma j) (nf_evar sigma ty)
 
-let rec execute mf env sigma cstr =
+let rec execute env evd cstr =
   match kind_of_term cstr with
     | Meta n ->
-	error "execute: found a non-instanciated goal"
+        { uj_val = cstr; uj_type = Evarutil.meta_type (snd evd) n }
 
     | Evar ev ->
-	let ty = Instantiate.existential_type sigma ev in
-	let jty = execute mf env sigma ty in
-	let jty = assumption_of_judgment env sigma jty in
+        let sigma = fst evd in
+	let ty = Evd.existential_type sigma ev in
+	let jty = execute env evd ty in
+	let jty = assumption_of_judgment env evd jty in
 	{ uj_val = cstr; uj_type = jty }
 	
     | Rel n -> 
@@ -62,22 +62,20 @@ let rec execute mf env sigma cstr =
 	make_judge cstr (type_of_constructor env cstruct)
 	  
     | Case (ci,p,c,lf) ->
-        let cj = execute mf env sigma c in
-        let pj = execute mf env sigma p in
-        let lfj = execute_array mf env sigma lf in
+        let cj = execute env evd c in
+        let pj = execute env evd p in
+        let lfj = execute_array env evd lf in
         let (j,_) = judge_of_case env ci pj cj lfj in
         j
   
     | Fix ((vn,i as vni),recdef) ->
-        if (not mf.fix) && array_exists (fun n -> n < 0) vn then
-          error "General Fixpoints not allowed";
-        let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in
+        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
 	let fix = (vni,recdef') in
         check_fix env fix;
 	make_judge (mkFix fix) tys.(i)
 	  
     | CoFix (i,recdef) ->
-        let (_,tys,_ as recdef') = execute_recdef mf env sigma recdef in
+        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
         let cofix = (i,recdef') in
         check_cofix env cofix;
 	make_judge (mkCoFix cofix) tys.(i)
@@ -89,86 +87,88 @@ let rec execute mf env sigma cstr =
 	judge_of_type u
 	  
     | App (f,args) ->
-	let j = execute mf env sigma f in
-        let jl = execute_array mf env sigma args in
+	let j = execute env evd f in
+        let jl = execute_array env evd args in
 	let (j,_) = judge_of_apply env j jl in
 	j
 	    
     | Lambda (name,c1,c2) -> 
-        let j = execute mf env sigma c1 in
-	let var = type_judgment env sigma j in
+        let j = execute env evd c1 in
+	let var = type_judgment env evd j in
 	let env1 = push_rel (name,None,var.utj_val) env in
-        let j' = execute mf env1 sigma c2 in 
+        let j' = execute env1 evd c2 in 
         judge_of_abstraction env1 name var j'
 	  
     | Prod (name,c1,c2) ->
-        let j = execute mf env sigma c1 in
-        let varj = type_judgment env sigma j in
+        let j = execute env evd c1 in
+        let varj = type_judgment env evd j in
 	let env1 = push_rel (name,None,varj.utj_val) env in
-        let j' = execute mf env1 sigma c2 in
-        let varj' = type_judgment env1 sigma j' in
+        let j' = execute env1 evd c2 in
+        let varj' = type_judgment env1 evd j' in
 	judge_of_product env name varj varj'
 
      | LetIn (name,c1,c2,c3) ->
-        let j1 = execute mf env sigma c1 in
-        let j2 = execute mf env sigma c2 in
-        let j2 = type_judgment env sigma j2 in
+        let j1 = execute env evd c1 in
+        let j2 = execute env evd c2 in
+        let j2 = type_judgment env evd j2 in
         let _ =  judge_of_cast env j1 j2 in
         let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
-        let j3 = execute mf env1 sigma c3 in
+        let j3 = execute env1 evd c3 in
         judge_of_letin env name j1 j2 j3
   
     | Cast (c,t) ->
-        let cj = execute mf env sigma c in
-        let tj = execute mf env sigma t in
-	let tj = type_judgment env sigma tj in
+        let cj = execute env evd c in
+        let tj = execute env evd t in
+	let tj = type_judgment env evd tj in
         let j, _ = judge_of_cast env cj tj in
 	j
 
-and execute_recdef mf env sigma (names,lar,vdef) =
-  let larj = execute_array mf env sigma lar in
-  let lara = Array.map (assumption_of_judgment env sigma) larj in
+and execute_recdef env evd (names,lar,vdef) =
+  let larj = execute_array env evd lar in
+  let lara = Array.map (assumption_of_judgment env evd) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let vdefj = execute_array mf env1 sigma vdef in
+  let vdefj = execute_array env1 evd vdef in
   let vdefv = Array.map j_val vdefj in
   let _ = type_fixpoint env1 names lara vdefj in
   (names,lara,vdefv)
 
-and execute_array mf env sigma v =
-  let jl = execute_list mf env sigma (Array.to_list v) in
+and execute_array env evd v =
+  let jl = execute_list env evd (Array.to_list v) in
   Array.of_list jl
 
-and execute_list mf env sigma = function
+and execute_list env evd = function
   | [] -> 
       []
   | c::r -> 
-      let j = execute mf env sigma c in 
-      let jr = execute_list mf env sigma r in
+      let j = execute env evd c in 
+      let jr = execute_list env evd r in
       j::jr
 
-
-let safe_machine env sigma constr = 
-  let mf = { fix = false; nocheck = false } in
-  execute mf env sigma constr
-
-let unsafe_machine env sigma constr =
-  let mf = { fix = false; nocheck = true } in
-  execute mf env sigma constr
+let mcheck env evd c t =
+  let j = execute env evd c in
+  check_type env evd j t
 
 (* Type of a constr *)
-
-let type_of env sigma c = 
-  let j = safe_machine env sigma c in 
+ 
+let mtype_of env evd c =
+  let j = execute env evd c in
   (* No normalization: it breaks Pattern! *)
   (*nf_betaiota*) (body_of_type j.uj_type)
 
-(* The typed type of a judgment. *)
+let msort_of env evd c =
+  let j = execute env evd c in
+  let a = type_judgment env evd j in
+  a.utj_type
 
-let execute_type env sigma constr = 
-  let j = execute { fix=false; nocheck=true } env sigma constr in
-  assumption_of_judgment env sigma j
+let type_of env sigma c =
+  mtype_of env (sigma, Evd.Metamap.empty) c
+let sort_of env sigma c =
+  msort_of env (sigma, Evd.Metamap.empty) c
+let check env sigma c   =
+  mcheck env (sigma, Evd.Metamap.empty) c
 
-let execute_rec_type env sigma constr = 
-  let j = execute { fix=false; nocheck=false } env sigma constr in
-  assumption_of_judgment env sigma j
+(* The typed type of a judgment. *)
 
+let mtype_of_type env evd constr =
+  let j = execute env evd constr in
+  assumption_of_judgment env evd j
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 8af977f104..15f3a6597a 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -17,11 +17,17 @@ open Evd
 (* This module provides the typing machine with existential variables
    (but without universes). *)
 
-val unsafe_machine : env -> evar_map -> constr -> unsafe_judgment
-
-val type_of : env -> evar_map -> constr -> constr
-
-val execute_type : env -> evar_map -> constr -> types
-
-val execute_rec_type : env -> evar_map -> constr -> types
-
+(* Typecheck a term and return its type *)
+val type_of : env -> evar_map -> constr -> types
+(* Typecheck a type and return its sort *)
+val sort_of : env -> evar_map -> types -> sorts
+(* Typecheck a term has a given type (assuming the type is OK *)
+val check   : env -> evar_map -> constr -> types -> unit
+ 
+(* The same but with metas... *)
+val mtype_of : env -> evar_map * meta_map -> constr -> types
+val msort_of : env -> evar_map * meta_map -> types -> sorts
+val mcheck   : env -> evar_map * meta_map -> constr -> types -> unit
+ 
+(* unused typing function... *)
+val mtype_of_type : env -> evar_map * meta_map -> types -> types
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
new file mode 100644
index 0000000000..8c33a07465
--- /dev/null
+++ b/pretyping/unification.ml
@@ -0,0 +1,488 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Environ
+open Evd
+open Reductionops
+open Rawterm
+open Pattern
+open Evarutil
+open Pretype_errors
+
+(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
+   gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
+
+let abstract_scheme env c l lname_typ =
+  List.fold_left2 
+    (fun t (locc,a) (na,_,ta) ->
+       let na = match kind_of_term a with Var id -> Name id | _ -> na in
+       if occur_meta ta then error "cannot find a type for the generalisation"
+       else if occur_meta a then lambda_name env (na,ta,t)
+       else lambda_name env (na,ta,subst_term_occ locc a t))
+    c
+    (List.rev l)
+    lname_typ
+
+let abstract_list_all env sigma typ c l =
+  let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in
+  let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in 
+  try 
+    if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p
+    else error "abstract_list_all"
+  with UserError _ ->
+    raise (PretypeError (env,CannotGeneralize typ))
+
+
+(*******************************)
+
+type maps = evar_map * meta_map
+
+(* [w_Define evd sp c]
+ *
+ * Defines evar [sp] with term [c] in evar context [evd].
+ * [c] is typed in the context of [sp] and evar context [evd] with
+ * [sp] removed to avoid circular definitions.
+ *)
+let w_Define evd sp c =
+  let sigma = evars_of evd in
+  if Evd.is_defined sigma sp then
+    error "Unify.w_Define: cannot define evar twice";
+  let spdecl = Evd.map sigma sp in
+  let env = evar_env spdecl in
+  let _ =
+    try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
+    with Not_found ->
+      error "Instantiation contains unlegal variables" in
+  let spdecl' = { spdecl with evar_body = Evar_defined c } in
+  evars_reset_evd (Evd.add sigma sp spdecl') evd
+
+
+(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
+   renvoie deux listes:
+
+   metasubst:(int*constr)list    récolte les instances des (Meta k)
+   evarsubst:(constr*constr)list récolte les instances des (Const "?k")
+
+   Attention : pas d'unification entre les différences instances d'une
+   même meta ou evar, il peut rester des doublons *)
+
+(* Unification order: *)
+(* Left to right: unifies first argument and then the other arguments *)
+(*let unify_l2r x = List.rev x
+(* Right to left: unifies last argument and then the other arguments *)
+let unify_r2l x = x
+
+let sort_eqns = unify_r2l
+*)
+
+let unify_0 env sigma cv_pb m n =
+  let trivial_unify pb substn m n =
+    if (not(occur_meta m)) & is_fconv pb env sigma m n then substn
+    else error_cannot_unify env sigma (m,n) in
+  let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n =
+    let cM = Evarutil.whd_castappevar sigma m
+    and cN = Evarutil.whd_castappevar sigma n in 
+    match (kind_of_term cM,kind_of_term cN) with
+      | Meta k1, Meta k2 ->
+	  if k1 < k2 then (k1,cN)::metasubst,evarsubst
+	  else if k1 = k2 then substn
+	  else (k2,cM)::metasubst,evarsubst
+      | Meta k, _    -> (k,cN)::metasubst,evarsubst
+      | _, Meta k    -> (k,cM)::metasubst,evarsubst
+      | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
+      | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
+
+      | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
+	  unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
+      | Prod (_,t1,c1), Prod (_,t2,c2) ->
+	  unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
+      | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
+      | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
+
+      | App (f1,l1), App (f2,l2) ->
+	  let len1 = Array.length l1
+	  and len2 = Array.length l2 in
+          let (f1,l1,f2,l2) =
+	    if len1 = len2 then (f1,l1,f2,l2)
+	    else if len1 < len2 then
+              let extras,restl2 = array_chop (len2-len1) l2 in 
+              (f1, l1, appvect (f2,extras), restl2)
+	    else 
+	      let extras,restl1 = array_chop (len1-len2) l1 in 
+              (appvect (f1,extras), restl1, f2, l2) in
+          (try
+            array_fold_left2 (unirec_rec CONV)
+	      (unirec_rec CONV substn f1 f2) l1 l2
+	  with ex when precatchable_exception ex ->
+            trivial_unify pb substn cM cN)
+      | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
+          array_fold_left2 (unirec_rec CONV)
+	    (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
+
+      | _ -> trivial_unify pb substn cM cN
+
+  in
+  if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then 
+    ([],[])
+  else 
+    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
+    ((*sort_eqns*) mc, (*sort_eqns*) ec)
+
+
+(* Unification
+ *
+ * Procedure:
+ * (1) The function [unify mc wc M N] produces two lists:
+ *     (a) a list of bindings Meta->RHS
+ *     (b) a list of bindings EVAR->RHS
+ *
+ * The Meta->RHS bindings cannot themselves contain
+ * meta-vars, so they get applied eagerly to the other
+ * bindings.  This may or may not close off all RHSs of
+ * the EVARs.  For each EVAR whose RHS is closed off,
+ * we can just apply it, and go on.  For each which
+ * is not closed off, we need to do a mimick step -
+ * in general, we have something like:
+ *
+ *      ?X == (c e1 e2 ... ei[Meta(k)] ... en)
+ *
+ * so we need to do a mimick step, converting ?X
+ * into
+ *
+ *      ?X -> (c ?z1 ... ?zn)
+ *
+ * of the proper types.  Then, we can decompose the
+ * equation into
+ *
+ *      ?z1 --> e1
+ *          ...
+ *      ?zi --> ei[Meta(k)]
+ *          ...
+ *      ?zn --> en
+ *
+ * and keep on going.  Whenever we find that a R.H.S.
+ * is closed, we can, as before, apply the constraint
+ * directly.  Whenever we find an equation of the form:
+ *
+ *      ?z -> Meta(n)
+ *
+ * we can reverse the equation, put it into our metavar
+ * substitution, and keep going.
+ *
+ * The most efficient mimick possible is, for each
+ * Meta-var remaining in the term, to declare a
+ * new EVAR of the same type.  This is supposedly
+ * determinable from the clausale form context -
+ * we look up the metavar, take its type there,
+ * and apply the metavar substitution to it, to
+ * close it off.  But this might not always work,
+ * since other metavars might also need to be resolved. *)
+
+let applyHead env sigma n c  = 
+  let evd = create_evar_defs sigma in
+  let rec apprec n c cty =
+    if n = 0 then 
+      (evars_of evd, c)
+    else 
+      match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
+        | Prod (_,c1,c2) ->
+            let evar =
+              Evarutil.new_isevar evd env
+                (dummy_loc,Rawterm.InternalHole) c1 in
+	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2)
+	| _ -> error "Apply_Head_Then"
+  in 
+  apprec n c (Typing.type_of env (evars_of evd) c)
+
+let is_mimick_head f =
+  match kind_of_term f with
+      (Const _|Var _|Rel _|Construct _|Ind _) -> true
+    | _ -> false
+
+let mimick_evar env evd hdc nargs sp =
+  let (sigma',c) = applyHead env (evars_of evd) nargs hdc in
+  evars_reset_evd sigma' evd;
+  w_Define evd sp c
+  
+
+(* [w_merge env sigma b metas evars] merges common instances in metas
+   or in evars, possibly generating new unification problems; if [b]
+   is true, unification of types of metas is required *)
+
+let w_merge env (sigma,metamap) with_types metas evars =
+  let evd = create_evar_defs sigma in
+  let mmap = ref metamap in
+  let ty_metas = ref [] in
+  let ty_evars = ref [] in
+  let rec w_merge_rec metas evars =
+    match (evars,metas) with
+      | ([], []) -> ()
+
+      | ((lhs,rhs)::t, metas) ->
+      (match kind_of_term rhs with
+
+	| Meta k -> w_merge_rec ((k,lhs)::metas) t
+
+	| krhs ->
+        (match kind_of_term lhs with
+
+	  | Evar (evn,_ as ev) ->
+    	      if is_defined_evar evd ev then
+		let (metas',evars') =
+                  unify_0 env (evars_of evd) CONV rhs lhs in
+		w_merge_rec (metas'@metas) (evars'@t)
+    	      else begin
+		let rhs' = 
+		  if occur_meta rhs then subst_meta metas rhs else rhs 
+		in
+		if occur_evar evn rhs' then
+                  error "w_merge: recursive equation";
+                match krhs with
+		  | App (f,cl) when is_mimick_head f ->
+		      (try 
+                        w_Define evd evn rhs'; 
+		        w_merge_rec metas t
+		      with ex when precatchable_exception ex ->
+                        mimick_evar env evd f (Array.length cl) evn;
+			w_merge_rec metas evars)
+                  | _ ->
+                      (* ensure tail recursion in non-mimickable case! *)
+                      w_Define evd evn rhs'; 
+		      w_merge_rec metas t
+	      end
+
+	  | _ -> anomaly "w_merge_rec"))
+
+      | ([], (mv,n)::t) ->
+    	  if meta_defined !mmap mv then
+            let (metas',evars') =
+              unify_0 env (evars_of evd) CONV (meta_fvalue !mmap mv).rebus n in
+            w_merge_rec (metas'@t) evars'
+    	  else
+            begin
+	      if with_types (* or occur_meta mvty *) then
+	        (let mvty = meta_type !mmap mv in
+		try 
+                  let sigma = evars_of evd in
+                  (* why not typing with the metamap ? *)
+		  let nty = Typing.type_of env sigma (nf_meta !mmap n) in
+		  let (mc,ec) = unify_0 env sigma CUMUL nty mvty in
+                  ty_metas := mc @ !ty_metas;
+                  ty_evars := ec @ !ty_evars
+		with e when precatchable_exception e -> ());
+              mmap := meta_assign mv n !mmap;
+	      w_merge_rec t []
+            end in
+  (* merge constraints *)
+  w_merge_rec metas evars;
+  (if with_types then
+    (* merge constraints about types: if they fail, don't worry *)
+    try w_merge_rec !ty_metas !ty_evars
+(* TODO: should backtrack *)
+    with e when precatchable_exception e -> ());
+  (evars_of evd, !mmap)
+
+(* [w_unify env evd M N]
+   performs a unification of M and N, generating a bunch of
+   unification constraints in the process.  These constraints
+   are processed, one-by-one - they may either generate new
+   bindings, or, if there is already a binding, new unifications,
+   which themselves generate new constraints.  This continues
+   until we get failure, or we run out of constraints.
+   [clenv_typed_unify M N clenv] expects in addition that expected
+   types of metavars are unifiable with the types of their instances    *)
+
+let w_unify_core_0 env evd with_types cv_pb m n =
+  let (mc,ec) = unify_0 env (fst evd) cv_pb m n in 
+  w_merge env evd with_types mc ec
+
+let w_unify_0 env evd = w_unify_core_0 env evd false
+let w_typed_unify env evd = w_unify_core_0 env evd true
+
+
+(* takes a substitution s, an open term op and a closed term cl
+   try to find a subterm of cl which matches op, if op is just a Meta
+   FAIL because we cannot find a binding *)
+
+let iter_fail f a =
+  let n = Array.length a in 
+  let rec ffail i =
+    if i = n then error "iter_fail" 
+    else
+      try f a.(i) 
+      with ex when precatchable_exception ex -> ffail (i+1)
+  in ffail 0
+
+(* Tries to find an instance of term [cl] in term [op].
+   Unifies [cl] to every subterm of [op] until it finds a match.
+   Fails if no match is found *)
+let w_unify_to_subterm env (op,cl) evd =
+  let rec matchrec cl =
+    let cl = strip_outer_cast cl in
+    (try 
+       if closed0 cl 
+       then w_unify_0 env evd CONV op cl,cl
+       else error "Bound 1"
+     with ex when precatchable_exception ex ->
+       (match kind_of_term cl with 
+	  | App (f,args) ->
+	      let n = Array.length args in
+	      assert (n>0);
+	      let c1 = mkApp (f,Array.sub args 0 (n-1)) in
+	      let c2 = args.(n-1) in
+	      (try 
+		 matchrec c1
+	       with ex when precatchable_exception ex -> 
+		 matchrec c2)
+          | Case(_,_,c,lf) -> (* does not search in the predicate *)
+	       (try 
+		 matchrec c
+	       with ex when precatchable_exception ex -> 
+		 iter_fail matchrec lf)
+	  | LetIn(_,c1,_,c2) -> 
+	       (try 
+		 matchrec c1
+	       with ex when precatchable_exception ex -> 
+		 matchrec c2)
+
+	  | Fix(_,(_,types,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when precatchable_exception ex -> 
+		 iter_fail matchrec terms)
+	
+	  | CoFix(_,(_,types,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when precatchable_exception ex -> 
+		 iter_fail matchrec terms)
+
+          | Prod (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when precatchable_exception ex -> 
+		 matchrec c)
+          | Lambda (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when precatchable_exception ex -> 
+		 matchrec c)
+          | _ -> error "Match_subterm")) 
+  in 
+  try matchrec cl
+  with ex when precatchable_exception ex ->
+    raise (PretypeError (env,NoOccurrenceFound op))
+
+let w_unify_to_subterm_list env allow_K oplist t evd = 
+  List.fold_right 
+    (fun op (evd,l) ->
+      if isMeta op then
+	if allow_K then (evd,op::l)
+	else error "Match_subterm"
+      else if occur_meta op then
+        let (evd',cl) =
+          try 
+	    (* This is up to delta for subterms w/o metas ... *)
+	    w_unify_to_subterm env (strip_outer_cast op,t) evd
+          with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
+        in 
+	(evd',cl::l)
+      else if not allow_K & not (dependent op t) then
+	(* This is not up to delta ... *)
+	raise (PretypeError (env,NoOccurrenceFound op))
+      else
+	(evd,op::l))
+    oplist 
+    (evd,[])
+
+let secondOrderAbstraction env evd allow_K typ (p, oplist) =
+  let sigma = fst evd in
+  let (evd',cllist) =
+    w_unify_to_subterm_list env allow_K oplist typ evd in
+  let typp = meta_type (snd evd') p in
+  let pred = abstract_list_all env sigma typp typ cllist in
+  w_unify_0 env evd' CONV (mkMeta p) pred
+
+let w_unify2 env evd allow_K cv_pb ty1 ty2 =
+  let c1, oplist1 = whd_stack ty1 in
+  let c2, oplist2 = whd_stack ty2 in
+  match kind_of_term c1, kind_of_term c2 with
+    | Meta p1, _ ->
+        (* Find the predicate *)
+	let evd' =
+          secondOrderAbstraction env evd allow_K ty2 (p1,oplist1) in 
+        (* Resume first order unification *)
+	w_unify_0 env evd' cv_pb (nf_meta (snd evd') ty1) ty2
+    | _, Meta p2 ->
+        (* Find the predicate *)
+	let evd' =
+          secondOrderAbstraction env evd allow_K ty1 (p2, oplist2) in 
+        (* Resume first order unification *)
+	w_unify_0 env evd' cv_pb ty1 (nf_meta (snd evd') ty2)
+    | _ -> error "w_unify2"
+
+
+(* The unique unification algorithm works like this: If the pattern is
+   flexible, and the goal has a lambda-abstraction at the head, then
+   we do a first-order unification.
+
+   If the pattern is not flexible, then we do a first-order
+   unification, too.
+
+   If the pattern is flexible, and the goal doesn't have a
+   lambda-abstraction head, then we second-order unification. *)
+
+(* We decide here if first-order or second-order unif is used for Apply *)
+(* We apply a term of type (ai:Ai)C and try to solve a goal C'          *)
+(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve    *)
+
+(* 3-4-99 [HH] New fo/so choice heuristic :
+   In case we have to unify (Meta(1) args) with ([x:A]t args')
+   we first try second-order unification and if it fails first-order.
+   Before, second-order was used if the type of Meta(1) and [x:A]t was
+   convertible and first-order otherwise. But if failed if e.g. the type of
+   Meta(1) had meta-variables in it. *)
+let w_unify allow_K env cv_pb ty1 ty2 evd =
+  let hd1,l1 = whd_stack ty1 in
+  let hd2,l2 = whd_stack ty2 in
+  match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
+    (* Pattern case *)
+    | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
+      when List.length l1 = List.length l2 ->
+	(try 
+	   w_typed_unify env evd cv_pb ty1 ty2
+	 with ex when precatchable_exception ex -> 
+	   try 
+	     w_unify2 env evd allow_K cv_pb ty1 ty2
+	   with PretypeError (env,NoOccurrenceFound c) as e -> raise e
+	     | ex when precatchable_exception ex -> 
+	     error "Cannot solve a second-order unification problem")
+
+     (* Second order case *)
+     | (Meta _, true, _, _ | _, _, Meta _, true) -> 
+	(try 
+	   w_unify2 env evd allow_K cv_pb ty1 ty2
+	with PretypeError (env,NoOccurrenceFound c) as e -> raise e
+	  | ex when precatchable_exception ex -> 
+          try 
+	     w_typed_unify env evd cv_pb ty1 ty2
+          with ex when precatchable_exception ex -> 
+             error "Cannot solve a second-order unification problem")
+
+     (* General case: try first order *)
+     | _ -> w_unify_0 env evd cv_pb ty1 ty2
+
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
new file mode 100644
index 0000000000..ae276b2a82
--- /dev/null
+++ b/pretyping/unification.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Environ
+open Evd
+(*i*)
+
+type maps = evar_map * meta_map
+
+val w_Define : Evarutil.evar_defs -> evar -> constr -> unit
+
+(* The "unique" unification fonction *)
+val w_unify :
+  bool -> env -> Reductionops.conv_pb -> constr -> constr -> maps -> maps
+
+(* [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 -> constr * constr -> maps -> maps * constr
+
+(*i This should be in another module i*)
+
+(* [abstract_list_all env sigma t c l]                     *)
+(* abstracts the terms in l over c to get a term of type t *)
+(* (used in inv.ml) *)
+val abstract_list_all :
+  env -> evar_map -> constr -> constr -> constr list -> constr