Imported Upstream version 8.1~gammaupstream/8.1.gamma

32 files changed, 971 insertions, 395 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b0fe83a3..58dda021 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
 
 open Util
 open Names
@@ -336,8 +336,8 @@ let inh_coerce_to_ind isevars env ty tyi =
         un inductif cela doit être égal *)
   let _ = e_cumul env isevars expected_typ ty in ()
 
-let unify_tomatch_with_patterns isevars env typ tm =
-  match find_row_ind tm with
+let unify_tomatch_with_patterns isevars env loc typ pats =
+  match find_row_ind pats with
     | None -> NotInd (None,typ)
     | Some (_,(ind,_)) ->
 	inh_coerce_to_ind isevars env typ ind;
@@ -345,29 +345,26 @@ let unify_tomatch_with_patterns isevars env typ tm =
 	with Not_found -> NotInd (None,typ)
 
 let find_tomatch_tycon isevars env loc = function
-  (* Try first if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_,_),_ 
-  (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
-  | None, Some (_,(ind,_)) ->
-      mk_tycon (inductive_template isevars env loc ind)
-  | None, None -> 
-      empty_tycon
-
-let coerce_row typing_fun isevars env cstropt (tomatch,(_,indopt)) =
+  (* Try if some 'in I ...' is present and can be used as a constraint *)
+  | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind)
+  | None -> empty_tycon
+
+let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
   let loc = Some (loc_of_rawconstr tomatch) in
-  let tycon = find_tomatch_tycon isevars env loc (indopt,cstropt) in
+  let tycon = find_tomatch_tycon isevars env loc indopt in
   let j = typing_fun tycon env tomatch in
   let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
-  let t = 
+  let t =
     try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
-    with Not_found -> NotInd (None,typ) in
+    with Not_found ->
+      unify_tomatch_with_patterns isevars env loc typ pats in
   (j.uj_val,t)
 
 let coerce_to_indtype typing_fun isevars env matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
   let matx' = match matrix_transpose pats with
-    | [] -> List.map (fun _ -> None) tomatchl (* no patterns at all *)
-    | m -> List.map find_row_ind m in
+    | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
+    | m -> m in
   List.map2 (coerce_row typing_fun isevars env) matx' tomatchl
 
 (************************************************************************)
@@ -500,12 +497,12 @@ let rec adjust_local_defs loc = function
   | [], [] -> []
   | _ -> raise NotAdjustable
 
-let check_and_adjust_constructor ind cstrs = function 
+let check_and_adjust_constructor env ind cstrs = function 
   | PatVar _ as pat -> pat
   | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
-      if ind' = ind then
+      if Closure.mind_equiv env ind' ind then
 	(* Check the constructor has the right number of args *)
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
@@ -1132,7 +1129,7 @@ let first_clause_irrefutable env = function
   | eqn::mat -> List.for_all (irrefutable env) eqn.patterns
   | _ -> false
 
-let group_equations pb mind current cstrs mat =
+let group_equations pb ind current cstrs mat =
   let mat =
     if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
   let brs = Array.create (Array.length cstrs) [] in
@@ -1142,7 +1139,7 @@ let group_equations pb mind current cstrs mat =
       (fun eqn () ->
 	 let rest = remove_current_pattern eqn in
 	 let pat = current_pattern eqn in
-	 match check_and_adjust_constructor mind cstrs pat with 
+	 match check_and_adjust_constructor pb.env ind cstrs pat with 
 	   | PatVar (_,name) -> 
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b6cce031..bbad005c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: classops.ml 8642 2006-03-17 10:09:02Z notin $ *)
+(* $Id: classops.ml 9257 2006-10-21 17:28:28Z herbelin $ *)
 
 open Util
 open Pp
@@ -154,7 +154,8 @@ let lookup_pattern_path_between (s,t) =
 	   coe.coe_value
        in 
        match kind_of_term c with
-	 | Construct sp -> (sp, coe.coe_param)
+	 | Construct cstr ->
+	     (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
 	 | _ -> raise Not_found) l
 
 (* find_class_type : constr -> cl_typ * int *)
@@ -207,7 +208,7 @@ let class_of env sigma t =
 
 let inductive_class_of ind = fst (class_info (CL_IND ind))
 
-let class_args_of c = snd (decompose_app c)
+let class_args_of c = snd (find_class_type c)
 
 let string_of_class = function
   | CL_FUN -> "Funclass"
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 6113ec2d..abe31e06 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: clenv.ml 9279 2006-10-25 15:51:24Z herbelin $ *)
 
 open Pp
 open Util
@@ -74,6 +74,26 @@ let clenv_get_type_of ce c =
       (meta_list ce.env) in
   Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
 
+exception NotExtensibleClause
+
+let clenv_push_prod cl =
+  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let rec clrec typ = match kind_of_term typ with
+    | Cast (t,_,_) -> clrec t
+    | Prod (na,t,u) ->
+	let mv = new_meta () in
+	let dep = dependent (mkRel 1) u in
+	let na' = if dep then na else Anonymous in
+	let e' = meta_declare mv t ~name:na' cl.env in
+	let concl = if dep then subst1 (mkMeta mv) u else u in
+	let def = applist (cl.templval.rebus,[mkMeta mv]) in
+	{ templval = mk_freelisted def;
+	  templtyp = mk_freelisted concl;
+	  env = e';
+	  templenv = cl.templenv }
+    | _ -> raise NotExtensibleClause
+  in clrec typ
+
 let clenv_environments evd bound c =
   let rec clrec (e,metas) n c =
     match n, kind_of_term c with
@@ -258,7 +278,20 @@ let connect_clenv gls clenv =
  * resolution can cause unification of already-existing metavars, and
  * of the fresh ones which get created.  This operation is a composite
  * of operations which pose new metavars, perform unification on
- * terms, and make bindings.  *)
+ * terms, and make bindings. 
+
+   Otherwise said, from 
+
+     [clenv] = [env;sigma;metas |- c:T]
+     [clenv'] = [env';sigma';metas' |- d:U]
+     [mv] = [mi] of type [Ti] in [metas]
+
+   then, if the unification of [Ti] and [U] produces map [rho], the
+   chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
+   [rho'] being [rho;mi:=d].
+
+   In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
+*)
 let clenv_fchain mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
@@ -412,18 +445,18 @@ let clenv_constrain_missing_args mlist clause =
 (****************************************************************)
 (* Clausal environment for an application *)
 
-let make_clenv_binding_gen n gls (c,t) = function
+let make_clenv_binding_gen hyps_only n gls (c,t) = function
   | ImplicitBindings largs ->
       let clause = mk_clenv_from_n gls n (c,t) in
-      clenv_constrain_dep_args (n <> None) clause largs
+      clenv_constrain_dep_args hyps_only clause largs
   | ExplicitBindings lbind ->
       let clause = mk_clenv_rename_from_n gls n (c,t) in
       clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_n gls n (c,t)
 
-let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
-let make_clenv_binding = make_clenv_binding_gen None
+let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
+let make_clenv_binding = make_clenv_binding_gen false None
 
 (****************************************************************)
 (* Pretty-print *)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index f585dfea..b5433cac 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: clenv.mli 7659 2005-12-17 21:07:17Z herbelin $ i*)
+(*i $Id: clenv.mli 9277 2006-10-25 13:02:22Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -17,6 +17,7 @@ open Environ
 open Evd
 open Evarutil
 open Mod_subst
+open Rawterm
 (*i*)
 
 (***************************************************************)
@@ -93,24 +94,41 @@ val clenv_missing : clausenv -> metavariable list
 
 (* defines metas corresponding to the name of the bindings *)
 val clenv_match_args :
-  constr Rawterm.explicit_bindings -> clausenv -> clausenv
+  constr explicit_bindings -> clausenv -> clausenv
 val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv
 
 (* start with a clenv to refine with a given term with bindings *)
 
-(* 1- the arity of the lemma is fixed *)
+(* the arity of the lemma is fixed *)
+(* the optional int tells how many prods of the lemma have to be used *)
+(* use all of them if None *)
 val make_clenv_binding_apply :
-  evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings ->
+  evar_info sigma -> int option -> constr * constr -> constr bindings ->
    clausenv
 val make_clenv_binding :
-  evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv
-
-(* other stuff *)
+  evar_info sigma -> constr * constr -> constr bindings -> clausenv
+
+(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
+   [lmetas] is a list of metas to be applied to a proof of [t] so that
+   it produces the unification pattern [ccl]; [sigma'] is [sigma]
+   extended with [lmetas]; if [n] is defined, it limits the size of
+   the list even if [ccl] is still a product; otherwise, it stops when
+   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
+   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
+   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
+   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
 val clenv_environments :
  evar_defs -> int option -> types -> evar_defs * constr list * types
+
+(* [clenv_environments_evars env sigma n t] does the same but returns
+   a list of Evar's defined in [env] and extends [sigma] accordingly *)
 val clenv_environments_evars :
  env -> evar_defs -> int option -> types -> evar_defs * constr list * types
 
+(* if the clause is a product, add an extra meta for this product *)
+exception NotExtensibleClause
+val clenv_push_prod : clausenv -> clausenv
+
 (***************************************************************)
 (* Pretty-print *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d0ee913f..cc74b0ad 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: coercion.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: coercion.ml 9257 2006-10-21 17:28:28Z herbelin $ *)
 
 open Util
 open Names
@@ -20,6 +20,7 @@ open Evarutil
 open Evarconv
 open Retyping
 open Evd
+open Termops
 
 module type S = sig
   (*s Coercions. *)
@@ -66,7 +67,14 @@ module Default = struct
   (* Typing operations dealing with coercions *)
   exception NoCoercion
 
-  let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
+  let whd_app_evar sigma t =
+    match kind_of_term t with
+      | App (f,l) -> mkApp (whd_evar sigma f,l)
+      | _ -> whd_evar sigma t
+
+  let class_of1 env isevars t =
+    let sigma = evars_of isevars in
+    class_of env sigma (whd_app_evar sigma t)
 
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
@@ -84,7 +92,6 @@ module Default = struct
       apply_rec [] funj.uj_type argl
 
   (* appliquer le chemin de coercions de patterns p *)
-
   let apply_pattern_coercion loc pat p =
     List.fold_left
       (fun pat (co,n) ->
@@ -100,7 +107,6 @@ module Default = struct
       apply_pattern_coercion loc pat p
 
   (* appliquer le chemin de coercions p à hj *)
-
   let apply_coercion env p hj typ_cl =
     try 
       fst (List.fold_left
@@ -120,22 +126,23 @@ module Default = struct
     let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
       match kind_of_term t with
 	| Prod (_,_,_) -> (isevars,j)
-	| Evar ev when not (is_defined_evar isevars ev) ->
+	| Evar ev ->
 	    let (isevars',t) = define_evar_as_arrow isevars ev in
 	      (isevars',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+ 	       let t,i1 = class_of1 env isevars j.uj_type in
       	       let p = lookup_path_to_fun_from i1 in
 		 (isevars,apply_coercion env p j t)
 	     with Not_found -> (isevars,j))
 
   let inh_tosort_force loc env isevars j =
     try
-      let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+      let t,i1 = class_of1 env isevars j.uj_type in
       let p = lookup_path_to_sort_from i1 in
       let j1 = apply_coercion env p j t in 
-	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+      let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in
+        (isevars,type_judgment env j2)
     with Not_found ->
       error_not_a_type_loc loc env (evars_of isevars) j
 
@@ -154,8 +161,8 @@ module Default = struct
   let inh_coerce_to_fail env isevars c1 v t =
     let v', t' =
       try 
-	let t1,i1 = class_of1 env (evars_of isevars) c1 in
-	let t2,i2 = class_of1 env (evars_of isevars) t in
+	let t1,i1 = class_of1 env isevars c1 in
+	let t2,i2 = class_of1 env isevars t in
 	let p = lookup_path_between (i2,i1) in
 	  match v with
 	      Some v -> 
@@ -166,64 +173,68 @@ module Default = struct
     in
       try (the_conv_x_leq env t' c1 isevars, v', t')
       with Reduction.NotConvertible -> raise NoCoercion
-  open Pp
+
   let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
     try (the_conv_x_leq env t c1 isevars, v, t)
     with Reduction.NotConvertible ->
-      (try 
-	 inh_coerce_to_fail env isevars c1 v t
-	 with NoCoercion ->
-	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
-	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
-		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
-		    let (evd',b) =
-		      match v' with 
-			  Some v' ->
-			    (match kind_of_term v' with
-			       | Lambda (x,v1,v2) ->
-				   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)  (* leq v1 u1? *)
-				    with Reduction.NotConvertible -> (isevars, None))
-			       | _  -> (isevars, None))
-			| None -> (isevars, None)
-		    in 
-		      (match b with
-			   Some (x, v1, v2) ->
-			     let env1 = push_rel (x,None,v1) env in
-			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
-						       (Some v2) t2 u2 in
-			       (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
-				mkProd (x, v1, t2'))
-			 | None ->
-			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
-			     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
-			     (* has type (name:u1)u2 (with v' recursively obtained) *)
-			     let name = (match name with 
-					   | Anonymous -> Name (id_of_string "x")
-					   | _ -> name) in
-			     let env1 = push_rel (name,None,u1) env in
-			     let (evd', v1', t1') =
-			       inh_conv_coerce_to_fail loc env1 isevars
-				 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) 
-			     in
-			     let (evd'', v2', t2') = 
-			       let v2 =
-				 match v with 
-				     Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
-				   | None -> None
-			       and evd', t2 =
-				 match v1' with 
-				     Some v1' -> evd', subst1 v1' t2
-				   | None -> 
-				       let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
-					 evd', subst1 ev t2
-			       in
-				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
-			     in
-			       (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
-				mkProd (name, u1, t2')))
-		| _ -> raise NoCoercion))
-	
+    try inh_coerce_to_fail env isevars c1 v t
+    with NoCoercion ->
+    match
+      kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
+      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1)
+    with
+    | Prod (_,t1,t2), Prod (name,u1,u2) -> 
+	let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
+	let (evd',b) =
+	  match v' with 
+	  | Some v' ->
+	      (match kind_of_term v' with
+	       | Lambda (x,v1,v2) ->
+		   (* sous-typage non contravariant: pas de "leq v1 u1" *)
+		   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)
+		   with Reduction.NotConvertible -> (isevars, None))
+	       | _  -> (isevars, None))
+	  | None -> (isevars, None)
+	in
+	(match b with
+	 | Some (x, v1, v2) ->
+	     let env1 = push_rel (x,None,v1) env in
+	     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+	       (Some v2) t2 u2 in
+	     (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
+	     mkProd (x, v1, t2'))
+	 | None ->
+	     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+	     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+	     (* has type (name:u1)u2 (with v' recursively obtained) *)
+	     let name = match name with 
+	       | Anonymous -> Name (id_of_string "x")
+	       | _ -> name
+	     in
+	     let env1 = push_rel (name,None,u1) env in
+	     let (evd', v1', t1') =
+	       inh_conv_coerce_to_fail loc env1 isevars
+		 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
+	     in
+	     let (evd'', v2', t2') = 
+	       let v2 =
+		 match v with 
+		 | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1'
+		 | None -> None
+	       and evd', t2 =
+		 match v1' with 
+		 | Some v1' -> evd', subst_term v1' t2
+		 | None -> 
+		     let evd', ev =
+		       new_evar evd' env ~src:(loc, InternalHole) t1' in
+		     evd', subst_term ev t2
+	       in
+	       inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+	     in
+	     (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
+	     mkProd (name, u1, t2')))
+    | _ -> raise NoCoercion
+
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj (n, t) =
     match n with
@@ -236,8 +247,7 @@ module Default = struct
 		error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
-	  let nf = nf_isevar evd' in
-	    (evd',{ uj_val = nf val'; uj_type = nf t })
+	    (evd',{ uj_val = val'; uj_type = t })
       | Some (init, cur) -> (isevars, cj)
       
     let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 458f5bd3..3c4a23ec 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,14 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 8793 2006-05-05 17:41:41Z barras $ *)
+(* $Id: evarconv.ml 9141 2006-09-15 10:07:01Z herbelin $ *)
 
+open Pp
 open Util
 open Names
 open Term
 open Closure
 open Reduction
 open Reductionops
+open Termops
 open Environ
 open Typing
 open Classops
@@ -83,7 +85,7 @@ let evar_apprec env isevars stack c =
       | Evar (n,_ as ev) when Evd.is_defined sigma n ->
 	  aux (Evd.existential_value sigma ev, stack)
       | _ -> (t, list_of_stack stack)
-  in aux (c, append_stack (Array.of_list stack) empty_stack)
+  in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env isevars c =
   let (t,stack as s) = Reductionops.whd_stack c in
@@ -126,7 +128,6 @@ let check_conv_record (t1,l1) (t2,l2) =
   with _ -> 
     raise Not_found
 
-
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
@@ -190,12 +191,7 @@ let rec evar_conv_x env isevars pbty term1 term2 =
   else 
     let (t1,l1) = apprec_nohdbeta env isevars term1 in
     let (t2,l2) = apprec_nohdbeta env isevars term2 in
-    if (head_is_embedded_evar isevars t1 & not(is_eliminator t2))
-      or (head_is_embedded_evar isevars t2 & not(is_eliminator t1))
-    then 
-      (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)) isevars, true)
-    else 
-      evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
+    evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
 
 and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
@@ -229,7 +225,20 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
-          if List.length l1 <= List.length l2 then
+	  if 
+	    is_unification_pattern_evar ev1 l1 & 
+	    not (occur_evar (fst ev1) (applist (term2,l2)))
+	  then
+	    (* Miller-Pfenning's patterns unification *)
+	    (* Preserve generality (except that CCI has no eta-conversion) *)
+	    let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+	    let t2 = solve_pattern_eqn env l1 t2 in
+	    solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	  else if
+            List.length l1 <= List.length l2
+	  then
+	    (* Try first-order unification *)
+	    (* (heuristic that gives acceptable results in practice) *)
 	    let (deb2,rest2) =
               list_chop (List.length l2-List.length l1) l2 in
             ise_and i
@@ -248,7 +257,20 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
-       	  if List.length l2 <= List.length l1 then
+	  if 
+	    is_unification_pattern_evar ev2 l2 & 
+	    not (occur_evar (fst ev2) (applist (term1,l1)))
+	  then
+	    (* Miller-Pfenning's patterns unification *)
+	    (* Preserve generality (except that CCI has no eta-conversion) *)
+	    let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+	    let t1 = solve_pattern_eqn env l2 t1 in
+	    solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	  else if
+       	    List.length l2 <= List.length l1
+	  then
+	    (* Try first-order unification *)
+	    (* (heuristic that gives acceptable results in practice) *)
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
             (* First compare extra args for better failure message *)
@@ -273,8 +295,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (try conv_record env i
              (try check_conv_record appr1 appr2
 	      with Not_found -> check_conv_record appr2 appr1)
-(* TODO: remove this _ !!! *)
-           with _ -> (i,false))
+           with Not_found -> (i,false))
 	and f4 i =
           (* heuristic: unfold second argument first, exception made
              if the first argument is a beta-redex (expand a constant
@@ -295,38 +316,39 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	ise_try isevars [f2; f3; f4]
 
     | Flexible ev1, Rigid _ ->
-       	if (List.length l1 <= List.length l2) then
-       	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
-          ise_and isevars
-            (* First compare extra args for better failure message *)
-            [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 rest2);
-             (fun i ->
-               (* Then instantiate evar unless already done by unifying args *)
-	       let t2 = applist(term2,deb2) in
-	       if is_defined_evar i ev1 then
-		 evar_conv_x env i pbty (mkEvar ev1) t2
-	       else
-		 solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
-        else (isevars,false)
+	if 
+	  is_unification_pattern_evar ev1 l1 & 
+	  not (occur_evar (fst ev1) (applist (term2,l2)))
+	then
+	  (* Miller-Pfenning's patterns unification *)
+	  (* Preserve generality (except that CCI has no eta-conversion) *)
+	  let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in
+	  let t2 = solve_pattern_eqn env l1 t2 in
+	  solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2)
+	else
+	  (* Postpone the use of an heuristic *)
+	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  true
+
     | Rigid _, Flexible ev2 ->
-        if List.length l2 <= List.length l1 then
-       	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
-          ise_and isevars
-            (* First compare extra args for better failure message *)
-            [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
-	     (fun i ->
-               (* Then instantiate evar unless already done by unifying args *)
-	       let t1 = applist(term1,deb1) in
-	       if is_defined_evar i ev2 then
-		 evar_conv_x env i pbty t1 (mkEvar ev2)
-	       else
-		 solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
-        else (isevars,false)
+	if 
+	  is_unification_pattern_evar ev2 l2 & 
+	  not (occur_evar (fst ev2) (applist (term1,l1)))
+	then
+	  (* Miller-Pfenning's patterns unification *)
+	  (* Preserve generality (except that CCI has no eta-conversion) *)
+	  let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in
+	  let t1 = solve_pattern_eqn env l2 t1 in
+	  solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1)
+	else
+	  (* Postpone the use of an heuristic *)
+	  add_conv_pb (pbty,applist(term1,l1),applist(term2,l2)) isevars,
+	  true
 
     | MaybeFlexible flex1, Rigid _ ->
 	let f3 i =
 	  (try conv_record env i (check_conv_record appr1 appr2)
-           with _ -> (i,false))
+           with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
@@ -337,8 +359,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	     
     | Rigid _ , MaybeFlexible flex2 -> 
 	let f3 i = 
-	  (try (conv_record env i (check_conv_record appr2 appr1))
-           with _ -> (i,false))
+	  (try conv_record env i (check_conv_record appr2 appr1)
+           with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
@@ -468,7 +490,51 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
          params1 params);
      (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
      (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
-    
+
+let first_order_unification env isevars pbty (term1,l1) (term2,l2) =
+  match kind_of_term term1, kind_of_term term2 with
+    | Evar ev1,_ when List.length l1 <= List.length l2 ->
+	let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+	ise_and isevars
+          (* First compare extra args for better failure message *)
+        [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
+	(fun i ->
+          (* Then instantiate evar unless already done by unifying args *)
+	  let t2 = applist(term2,deb2) in
+	  if is_defined_evar i ev1 then
+	    evar_conv_x env i pbty t2 (mkEvar ev1)
+	  else
+	    solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))]
+    | _,Evar ev2 when List.length l2 <= List.length l1 ->
+	let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+	ise_and isevars
+          (* First compare extra args for better failure message *)
+        [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2);
+	(fun i ->
+          (* Then instantiate evar unless already done by unifying args *)
+	  let t1 = applist(term1,deb1) in
+	  if is_defined_evar i ev2 then
+	    evar_conv_x env i pbty t1 (mkEvar ev2)
+	  else
+	    solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))]
+    | _ -> 
+	(* Some head evar have been instantiated *)
+	evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2))
+
+let consider_remaining_unif_problems env isevars =
+  let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in
+  List.fold_left
+    (fun (isevars,b as p) (pbty,t1,t2) ->
+      (* Pas le bon env pour le problème... *)
+      if b then first_order_unification env isevars pbty 
+	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1))
+	(apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2))
+      else p)
+    (isevars,true)
+    pbs
+
+(* Main entry points *)
+
 let the_conv_x     env t1 t2 isevars =
   match evar_conv_x env isevars CONV  t1 t2 with
       (evd',true) -> evd'
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index a6f5b489..f92a6fdb 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarconv.mli 6109 2004-09-15 16:50:56Z barras $ i*)
+(*i $Id: evarconv.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
 
 (*i*)
 open Term
@@ -33,3 +33,5 @@ val evar_eqappr_x :
     conv_pb -> constr * constr list -> constr * constr list ->
       evar_defs * bool
 (*i*)
+
+val consider_remaining_unif_problems : env -> evar_defs -> evar_defs * bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 506cd03f..307c9886 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: evarutil.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Util
 open Pp
@@ -21,13 +21,6 @@ open Evd
 open Reductionops
 open Pretype_errors
 
-
-let rec filter_unique = function
-  | [] -> []
-  | x::l ->
-      if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
-      else x::filter_unique l
-
 (* Expanding existential variables (pretyping.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
 
@@ -63,9 +56,9 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar
 let tj_nf_evar = Pretype_errors.tj_nf_evar
 
 let nf_evar_info evc info =
-  { evar_concl = Reductionops.nf_evar evc info.evar_concl;
-    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
-    evar_body = info.evar_body}
+  { info with 
+      evar_concl = Reductionops.nf_evar evc info.evar_concl;
+      evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
 
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
@@ -310,29 +303,45 @@ let is_defined_equation env evd (ev,inst) rhs =
  * ?3 <-- ?1          no pb: env of ?3 is larger than ?1's
  * ?1 <-- (list ?2)   pb: ?2 may depend on x, but not ?1.
  * What we do is that ?2 is defined by a new evar ?4 whose context will be
- * a prefix of ?2's env, included in ?1's env. *)
+ * a prefix of ?2's env, included in ?1's env.
+
+ Concretely, the assumptions are "env |- ev : T" and "Gamma |-
+ ev[hyps:=args]" for some Gamma whose de Bruijn context has length k.
+ We create "env' |- ev' : T" for some env' <= env and define ev:=ev'
+*)
 
-let do_restrict_hyps evd ev args =
+let do_restrict_hyps env k evd ev args =
   let args = Array.to_list args in
   let evi = Evd.find (evars_of !evd) ev in
-  let env = evar_env evi in
   let hyps = evar_context evi in
-  let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in
+  let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in
   (* No care is taken in case the evar type uses vars filtered out!
-     Is it important ? *)
-  let nc =
-    let env =
-      Sign.fold_named_context push_named sign ~init:(reset_context env) in
-    e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in
+     Assuming that the restriction comes from a well-typed Flex/Flex
+     unification problem (see real_clean), the type of the evar cannot
+     depend on variables that are not in the scope of the other evar,
+     since this other evar has the same type (up to unification).
+     Since moreover, the evar contexts uses names only, the
+     restriction raise no de Bruijn reallocation problem *)
+  let env' =
+    Sign.fold_named_context push_named hyps' ~init:(reset_context env) in
+  let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in
   evd := Evd.evar_define ev nc !evd;
   let (evn,_) = destEvar nc in
   mkEvar(evn,Array.of_list ncargs)
 
-
-let need_restriction isevars args = not (array_for_all closed0 args)
+let need_restriction k args = not (array_for_all (closedn k) args)
 
 (* We try to instantiate the evar assuming the body won't depend
- * on arguments that are not Rels or Vars, or appearing several times.
+ * on arguments that are not Rels or Vars, or appearing several times
+   (i.e. we tackle only Miller-Pfenning patterns unification) 
+
+  1) Let a unification problem "env |- ev[hyps:=args] = rhs"
+  2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
+     where only Rel's and Var's are relevant in subst
+  3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope
+
+  Note: we don't assume rhs in normal form, it may fail while it would
+  have succeeded after some reductions
  *)
 (* Note: error_not_clean should not be an error: it simply means that the
  * conversion test that lead to the faulty call to [real_clean] should return
@@ -341,36 +350,52 @@ let need_restriction isevars args = not (array_for_all closed0 args)
 
 let real_clean env isevars ev evi args rhs =
   let evd = ref isevars in
-  let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
+  let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in
   let rec subs rigid k t =
     match kind_of_term t with
       | Rel i ->
  	 if i<=k then t
- 	 else (try List.assoc (mkRel (i-k)) subst with Not_found -> t)
+ 	 else
+	   (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *)
+	   (try List.assoc (mkRel (i-k)) subst 
+	    with Not_found -> if rigid then raise Exit else t)
       | Evar (ev,args) ->
           if Evd.is_defined_evar !evd (ev,args) then
             subs rigid k (existential_value (evars_of !evd) (ev,args))
           else
+	    (* Flex/Flex problem: restriction to a common scope *)
 	    let args' = Array.map (subs false k) args in
-	    if need_restriction !evd args' then
-              do_restrict_hyps evd ev args'
+	    if need_restriction k args' then
+              do_restrict_hyps (reset_context env) k evd ev args'
 	    else
 	      mkEvar (ev,args')
       | Var id ->
+	  (* Flex/Var problem: unifiable as a pattern iff Var in scope of ev *)
           (try List.assoc t subst
            with Not_found ->
              if
                not rigid 
+	     (* I don't understand this line: vars from evar_context evi
+		are private (especially some of them are freshly
+		generated in push_rel_context_to_named_context). They
+		have a priori nothing to do with the vars in env. I
+		remove the test [HH 25/8/06]
+
 		 or List.exists (fun (id',_,_) -> id=id') (evar_context evi)
+	     *)
              then t
-             else
-               error_not_clean env (evars_of !evd) ev rhs
-                 (evar_source ev !evd))
-      | _ -> map_constr_with_binders succ (subs rigid) k t
+             else raise Exit)
+               
+      | _ ->
+	  (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *)
+	  map_constr_with_binders succ (subs rigid) k t
   in
-  let body = subs true 0 (nf_evar (evars_of isevars) rhs) in
-  if not (closed0 body)
-  then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd);
+  let rhs = nf_evar (evars_of isevars) rhs in
+  let rhs = whd_beta rhs (* heuristic *) in
+  let body = 
+    try subs true 0 rhs
+    with Exit -> 
+      error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in
   (!evd,body)
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
@@ -464,6 +489,34 @@ let head_evar =
   in 
   hrec 
 
+(* Check if an applied evar "?X[args] l" is a Miller's pattern; note
+   that we don't care whether args itself contains Rel's or even Rel's
+   distinct from the ones in l *)
+
+let is_unification_pattern_evar (_,args) l =
+  let l' = Array.to_list args @ l in
+  List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l'
+
+let is_unification_pattern f l =
+  match kind_of_term f with
+    | Meta _ -> array_for_all isRel l & array_distinct l
+    | Evar ev -> is_unification_pattern_evar ev (Array.to_list l)
+    | _ -> false
+
+(* From a unification problem "?X l1 = term1 l2" such that l1 is made
+   of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
+
+let solve_pattern_eqn env l1 c =
+  let c' = List.fold_right (fun a c ->
+    let c' = subst_term (lift 1 a) (lift 1 c) in
+    match kind_of_term a with
+      (* Rem: if [a] links to a let-in, do as if it were an assumption *)
+      | Rel n -> let (na,_,t) = lookup_rel n env in mkLambda (na,lift n t,c')
+      | Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c'
+      | _ -> assert false) 
+    l1 c in
+  whd_eta c'
+
 (* This code (i.e. solve_pb, etc.) takes a unification
  * problem, and tries to solve it. If it solves it, then it removes
  * all the conversion problems, and re-runs conversion on each one, in
@@ -550,11 +603,28 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
     List.fold_left
       (fun (isevars,b as p) (pbty,t1,t2) ->
-        if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
+	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
       pbs
   with e when precatchable_exception e ->
     (isevars,false)
 
+
+(* [check_evars] fails if some unresolved evar remains *)
+(* it assumes that the defined existentials have already been substituted *)
+
+let check_evars env initial_sigma isevars c =
+  let sigma = evars_of isevars in
+  let c = nf_evar sigma c in
+  let rec proc_rec c =
+    match kind_of_term c with
+      | Evar (ev,args) ->
+          assert (Evd.mem sigma ev);
+	  if not (Evd.mem initial_sigma ev) then
+            let (loc,k) = evar_source ev isevars in
+	    error_unsolvable_implicit loc env sigma k
+      | _ -> iter_constr proc_rec c
+  in proc_rec c
+
 (* Operations on value/type constraints *)
 
 type type_constraint_type = (int * int) option * constr
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7429cd16..3ac05481 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evarutil.mli 8695 2006-04-10 16:33:52Z msozeau $ i*)
+(*i $Id: evarutil.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -78,10 +78,18 @@ val solve_simple_eqn :
   -> env ->  evar_defs -> conv_pb * existential * constr ->
     evar_defs * bool
 
+(* [check_evars env initial_sigma extended_sigma c] fails if some
+   new unresolved evar remains in [c] *)
+val check_evars : env -> evar_map -> evar_defs -> constr -> unit
+
 val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types
 val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
 val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
+val is_unification_pattern_evar : existential -> constr list -> bool
+val is_unification_pattern : constr -> constr array -> bool
+val solve_pattern_eqn : env -> constr list -> constr -> constr
+
 (***********************************************************)
 (* Value/Type constraints *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 33f88ebd..030983e1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evd.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: evd.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Pp
 open Util
@@ -30,7 +30,8 @@ type evar_body =
 type evar_info = {
   evar_concl : constr;
   evar_hyps : named_context_val;
-  evar_body : evar_body}
+  evar_body : evar_body;
+  evar_extra : Dyn.t option}
 
 let evar_context evi = named_context_of_val evi.evar_hyps
 
@@ -46,7 +47,11 @@ type evar_map1 = evar_info Evarmap.t
 
 let empty = Evarmap.empty
 
-let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let to_list evc = (* Workaround for change in Map.fold behavior *)
+  let l = ref [] in 
+    Evarmap.iter (fun ev x -> l:=(ev,x)::!l) evc;
+    !l
+
 let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
 let find evc k = Evarmap.find k evc
 let remove evc k = Evarmap.remove k evc
@@ -60,9 +65,8 @@ let define evd ev body =
     try find evd ev
     with Not_found -> error "Evd.define: cannot define undeclared evar" in
   let newinfo =
-    { evar_concl = oldinfo.evar_concl;
-      evar_hyps = oldinfo.evar_hyps;
-      evar_body = Evar_defined body} in
+    { oldinfo with
+      evar_body = Evar_defined body } in
   match oldinfo.evar_body with
     | Evar_empty -> Evarmap.add ev newinfo evd
     | _ -> anomaly "Evd.define: cannot define an isevar twice"
@@ -377,14 +381,7 @@ let create_evar_defs sigma =
 let evars_of d = d.evars
 let evars_reset_evd evd d = {d with evars = evd}
 let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
-let add_conv_pb pb d =
-(*  let (pbty,c1,c2) = pb in
-  pperrnl
-    (Termops.print_constr c1 ++
-    (if pbty=Reduction.CUMUL then str " <="++ spc()
-    else str" =="++spc()) ++
-    Termops.print_constr c2);*)
-  {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source ev d =
   try List.assoc ev d.history
   with Not_found -> (dummy_loc, InternalHole)
@@ -396,7 +393,10 @@ let evar_define sp body isevars =
 let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
   { evd with
     evars = add evd.evars evn
-      {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty};
+      {evar_hyps=hyps; 
+       evar_concl=ty; 
+       evar_body=Evar_empty; 
+       evar_extra=None};
     history = (evn,src)::evd.history }
 
 let is_defined_evar isevars (n,_) = is_defined isevars.evars n
@@ -548,14 +548,21 @@ let pr_evar_map sigma =
         h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
       (to_list sigma))
 
+let pr_constraints pbs =
+  h 0
+    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+      print_constr t1 ++ spc() ++
+      str (match pbty with
+	| Reduction.CONV -> "=="
+	| Reduction.CUMUL -> "<=") ++ 
+      spc() ++ print_constr t2) pbs)
+
 let pr_evar_defs evd =
   let pp_evm =
     if evd.evars = empty then mt() else
       str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in
-  let n = List.length evd.conv_pbs in
   let cstrs =
-    if n=0 then mt() else
-      str"=> " ++ int n ++ str" constraints" ++ fnl() ++ fnl() in
+    str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
   let pp_met =
     if evd.metas = Metamap.empty then mt() else
       str"METAS:"++brk(0,1)++pr_meta_map evd.metas in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index cbc96b04..876c34d2 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: evd.mli 8759 2006-04-28 12:24:14Z herbelin $ i*)
+(*i $Id: evd.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 (*i*)
 open Util
@@ -32,7 +32,8 @@ type evar_body =
 type evar_info = {
   evar_concl : constr;
   evar_hyps : Environ.named_context_val;
-  evar_body : evar_body}
+  evar_body : evar_body;
+  evar_extra : Dyn.t option}
 
 val eq_evar_info : evar_info -> evar_info -> bool
 val evar_context : evar_info -> named_context
@@ -94,6 +95,7 @@ type 'a freelisted = {
   rebus : 'a;
   freemetas : Metaset.t }
 
+val metavars_of : constr -> Metaset.t
 val mk_freelisted : constr -> constr freelisted
 val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e0cdeeee..14136f61 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: inductiveops.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Util
 open Names
@@ -23,7 +23,7 @@ open Reductionops
 
 let type_of_inductive env ind =
  let specif = Inductive.lookup_mind_specif env ind in
-  Inductive.type_of_inductive specif
+  Inductive.type_of_inductive env specif
 
 (* Return type as quoted by the user *)
 let type_of_constructor env cstr =
@@ -126,6 +126,10 @@ let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mib.mind_nparams, mip.mind_nrealargs
 
+let allowed_sorts env (kn,i as ind) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_kelim
+
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index dcd86716..d49b64d9 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductiveops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: inductiveops.mli 9194 2006-10-01 09:25:19Z herbelin $ i*)
 
 open Names
 open Term
@@ -66,6 +66,8 @@ val constructor_nrealhyps : env -> constructor -> int
 
 val get_full_arity_sign : env -> inductive -> rel_context
 
+val allowed_sorts : env -> inductive -> sorts_family list
+
 (* Extract information from an inductive family *)
 
 type constructor_summary = {
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 12c1ea33..65ce2ef4 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: matching.ml 8827 2006-05-17 15:15:34Z jforest $ *)
+(* $Id: matching.ml 9280 2006-10-25 21:37:37Z herbelin $ *)
 
 (*i*)
 open Util
@@ -119,6 +119,8 @@ let matches_core convert allow_partial_app pat c =
 
       | PSort (RType _), Sort (Type _) -> sigma
 
+      | PApp (p, [||]), _ -> sorec stk sigma p t
+
       | PApp (PApp (h, a1), a2), _ ->
           sorec stk sigma (PApp(h,Array.append a1 a2)) t
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f5a81659..59cdad04 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretype_errors.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
+(* $Id: pretype_errors.ml 9217 2006-10-05 17:31:23Z notin $ *)
 
 open Util
 open Stdpp
@@ -27,6 +27,7 @@ type pretype_error =
   | NotClean of existential_key * constr * Evd.hole_kind
   | UnsolvableImplicit of Evd.hole_kind
   | CannotUnify of constr * constr
+  | CannotUnifyLocal of Environ.env * constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr
@@ -157,6 +158,9 @@ let error_unsolvable_implicit loc env sigma e =
 let error_cannot_unify env sigma (m,n) =
   raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
 
+let error_cannot_unify_local env sigma (e,m,n,sn) = 
+  raise (PretypeError (env_ise sigma env,CannotUnifyLocal (e,m,n,sn)))
+
 let error_cannot_coerce env sigma (m,n) =
   raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 3c78d48d..137ef639 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretype_errors.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: pretype_errors.mli 9217 2006-10-05 17:31:23Z notin $ i*)
 
 (*i*)
 open Pp
@@ -29,6 +29,7 @@ type pretype_error =
   | NotClean of existential_key * constr * Evd.hole_kind
   | UnsolvableImplicit of Evd.hole_kind
   | CannotUnify of constr * constr
+  | CannotUnifyLocal of Environ.env * constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr
@@ -96,6 +97,8 @@ val error_unsolvable_implicit :
 
 val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
 
+val error_cannot_unify_local : env -> Evd.evar_map -> Environ.env * constr * 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 e3cfe974..0b00c82c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 8992 2006-06-27 21:29:18Z herbelin $ *)
+(* $Id: pretyping.ml 9338 2006-11-03 13:09:53Z herbelin $ *)
 
 open Pp
 open Util
@@ -245,6 +245,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let ccl' = mkLambda (Anonymous, ind, ccl) in
       {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 
 
+  let evar_kind_of_term sigma c =
+    kind_of_term (whd_evar (Evd.evars_of sigma) c)
+
   (*************************************************************************)
   (* Main pretyping function                                               *)
 
@@ -375,10 +378,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  | Prod (na,c1,c2) ->
 		      let hj = pretype (mk_tycon c1) env isevars lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
-		      let typ' = nf_isevar !isevars typ in
 			apply_rec env (n+1) 
-			  { uj_val = nf_isevar !isevars value;
-			    uj_type = typ' }
+			  { uj_val = value;
+			    uj_type = typ }
 			  rest
 		  | _ ->
 		      let hj = pretype empty_tycon env isevars lvar c in
@@ -386,15 +388,18 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj args) in
+	let resj = apply_rec env 1 fj args in
 	let resj =
-	  match kind_of_term resj.uj_val with
-	  | App (f,args) when isInd f ->
-	      let sigma = evars_of !isevars in
-	      let t = Retyping.type_of_inductive_knowing_parameters env sigma (destInd f) args in
-	      let s = snd (splay_arity env sigma t) in
-	      on_judgment_type (set_inductive_level env s) resj
-		(* Rem: no need to send sigma: no head evar, it's an arity *)
+	  match evar_kind_of_term !isevars resj.uj_val with
+	  | App (f,args) ->
+              let f = whd_evar (Evd.evars_of !isevars) f in
+              begin match kind_of_term f with
+              | Ind _ (* | Const _ *) ->
+	          let sigma = evars_of !isevars in
+		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
+	          let t = Retyping.get_type_of env sigma c in
+		  make_judge c t
+              | _ -> resj end
 	  | _ -> resj in
 	inh_conv_coerce_to_tycon loc env isevars resj tycon
 
@@ -455,7 +460,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 | Some p ->
 		     let env_p = push_rels psign env in
 		     let pj = pretype_type empty_valcon env_p isevars lvar p in
-		     let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+		     let ccl = nf_isevar !isevars pj.utj_val in
 		     let psign = make_arity_signature env true indf in (* with names *)
 		     let p = it_mkLambda_or_LetIn ccl psign in
 		     let inst = 
@@ -475,7 +480,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let tycon = lift_tycon cs.cs_nargs tycon in
 		     let fj = pretype tycon env_f isevars lvar d in
 		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-		     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
+		     let ccl = nf_isevar !isevars fj.uj_type in
 		     let ccl =
 		       if noccur_between 1 cs.cs_nargs ccl then
 			 lift (- cs.cs_nargs) ccl 
@@ -632,35 +637,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
       nf_evar (evars_of !isevars) c'
 
-  (* [check_evars] fails if some unresolved evar remains *)
-  (* it assumes that the defined existentials have already been substituted
-     (should be done in unsafe_infer and unsafe_infer_type) *)
-
-  let check_evars env initial_sigma isevars c =
-    let sigma = evars_of !isevars in
-    let rec proc_rec c =
-      match kind_of_term c with
-	| Evar (ev,args) ->
-            assert (Evd.mem sigma ev);
-	    if not (Evd.mem initial_sigma ev) then
-              let (loc,k) = evar_source ev !isevars in
-		error_unsolvable_implicit loc env sigma k
-	| _ -> iter_constr proc_rec c
-    in
-      proc_rec c(*;
-		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
-		  if pbs <> [] then begin
-		  pperrnl
-		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
-		  prlist_with_sep fnl
-		  (fun  (pb,c1,c2) ->
-		  Termops.print_constr c1 ++
-		  (if pb=Reduction.CUMUL then str " <="++ spc()
-		  else str" =="++spc()) ++
-		  Termops.print_constr c2)
-		  pbs ++ fnl())
-		  end*)
-
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -669,7 +645,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let isevars = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env isevars ([],[]) c in
-    let j = j_nf_evar (evars_of !isevars) j in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let j = j_nf_evar (evars_of isevars) j in
       check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
 
@@ -686,8 +663,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let c = nf_evar (evars_of isevars) c in
       if fail_evar then check_evars env sigma isevars c;
-      !isevars, c
+      isevars, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7bb8c374..b1ed20c2 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretyping.mli 8688 2006-04-07 15:08:12Z msozeau $ i*)
+(*i $Id: pretyping.mli 9141 2006-09-15 10:07:01Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -78,7 +78,6 @@ sig
   (* Idem but do not fail on unresolved evars *)
   val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
-       
   (*i*)
   (* Internal of Pretyping...
    *)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index ece536d1..00dd034d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml 8969 2006-06-22 12:51:04Z msozeau $ *)
+(* $Id: rawterm.ml 9226 2006-10-09 16:11:01Z herbelin $ *)
 
 (*i*)
 open Util
@@ -26,7 +26,7 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
-let pattern_loc = function
+let cases_pattern_loc = function
     PatVar(loc,_) -> loc
   | PatCstr(loc,_,_,_) -> loc
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 89b13ff0..6c2276d7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rawterm.mli 8969 2006-06-22 12:51:04Z msozeau $ i*)
+(*i $Id: rawterm.mli 9226 2006-10-09 16:11:01Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -17,7 +17,8 @@ open Libnames
 open Nametab
 (*i*)
 
-(* Untyped intermediate terms, after ASTs and before constr. *)
+(**********************************************************************)
+(* The kind of patterns that occurs in "match ... with ... end"       *)
 
 (* locs here refers to the ident's location, not whole pat *)
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
@@ -25,7 +26,13 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
-val pattern_loc : cases_pattern -> loc
+val cases_pattern_loc : cases_pattern -> loc
+
+(**********************************************************************)
+(* Untyped intermediate terms, after constr_expr and before constr    *)
+(* Resolution of names, insertion of implicit arguments placeholder,  *)
+(* and notations are done, but coercions, inference of implicit       *)
+(* arguments and pattern-matching compilation are not                 *)
 
 type patvar = identifier
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 74df5eea..5bbaa207 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: recordops.ml 9032 2006-07-07 16:30:34Z herbelin $ *)
+(* $Id: recordops.ml 9166 2006-09-23 11:20:06Z herbelin $ *)
 
 open Util
 open Pp
@@ -20,6 +20,7 @@ open Libobject
 open Library
 open Classops
 open Mod_subst
+open Reductionops
 
 (*s A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
@@ -78,7 +79,7 @@ let (inStruc,outStruc) =
     discharge_function = discharge_structure;
     export_function = (function x -> Some x) }
 
-let declare_structure (s,c,_,kl,pl) = 
+let declare_structure (s,c,kl,pl) = 
   Lib.add_anonymous_leaf (inStruc (s,c,kl,pl))
 
 let lookup_structure indsp = Indmap.find indsp !structure_table
@@ -197,7 +198,8 @@ let check_and_decompose_canonical_structure ref =
   let vc = match Environ.constant_opt_value env sp with
     | Some vc -> vc
     | None -> error_not_structure ref in
-  let f,args = match kind_of_term (snd (decompose_lam vc)) with
+  let body = snd (splay_lambda (Global.env()) Evd.empty vc) in
+  let f,args = match kind_of_term body with
     | App (f,args) -> f,args
     | _ -> error_not_structure ref in
   let indsp = match kind_of_term f with
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 91bc2ba1..0a05aef6 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: recordops.mli 9032 2006-07-07 16:30:34Z herbelin $ i*)
+(*i $Id: recordops.mli 9082 2006-08-24 17:03:28Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -22,7 +22,7 @@ open Library
    constructor (the name of which defaults to Build_S) *)
 
 val declare_structure : 
-  inductive * identifier * int * bool list * constant option list -> unit
+  inductive * identifier * bool list * constant option list -> unit
 
 (* [lookup_projections isp] returns the projections associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 82cc1b7d..19f515d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reductionops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: reductionops.ml 9106 2006-09-01 11:18:17Z herbelin $ *)
 
 open Pp
 open Util
@@ -37,11 +37,12 @@ type 'a stack_member =
 and 'a stack = 'a stack_member list
 
 let empty_stack = []
-let append_stack_list = function
+let append_stack_list l s =
+  match (l,s) with
   | ([],s) -> s
   | (l1, Zapp l :: s) -> Zapp (l1@l) :: s
   | (l1, s) -> Zapp l1 :: s
-let append_stack v s = append_stack_list (Array.to_list v, s)
+let append_stack v s = append_stack_list (Array.to_list v) s
 
 (* Collapse the shifts in the stack *)
 let zshift n s =
@@ -227,6 +228,7 @@ open RedFlags
 
 (* Local *)
 let beta = mkflags [fbeta]
+let eta = mkflags [feta]
 let evar = mkflags [fevar]
 let betaevar = mkflags [fevar; fbeta]
 let betaiota = mkflags [fiota; fbeta]
@@ -251,7 +253,7 @@ let rec stacklam recfun env t stack =
     | _ -> recfun (substl env t, stack)
 
 let beta_applist (c,l) =
-  stacklam app_stack [] c (append_stack (Array.of_list l) empty_stack)
+  stacklam app_stack [] c (append_stack_list l empty_stack)
 
 (* Iota reduction tools *)
 
@@ -261,7 +263,7 @@ type 'a miota_args = {
   mci     : case_info;  (* special info to re-build pattern *)
   mcargs  : 'a list;    (* the constructor's arguments *)
   mlf     : 'a array }  (* the branch code vector *)
-		       
+
 let reducible_mind_case c = match kind_of_term c with
   | Construct _ | CoFix _ -> true
   | _  -> false
@@ -505,6 +507,10 @@ let whd_betadeltaiota_nolet_stack env sigma x =
 let whd_betadeltaiota_nolet env sigma x = 
   app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
 
+(* 3. Eta reduction Functions *)
+
+let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
+
 (****************************************************************************)
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
@@ -641,7 +647,7 @@ let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
 let whd_meta metamap c = match kind_of_term c with
   | Meta p -> (try List.assoc p metamap with Not_found -> c)
   | _ -> c
-	
+
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
 let plain_instance s c = 
@@ -668,7 +674,7 @@ let plain_instance s c =
     | _ -> map_constr irec u
   in 
   if s = [] then c else irec c
-    
+
 (* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
 let instance s c = 
   if s = [] then c else local_strong whd_betaiota (plain_instance s c)
@@ -746,7 +752,7 @@ let splay_arity env sigma c =
     | _ -> error "not an arity"
 
 let sort_of_arity env c = snd (splay_arity env Evd.empty c)
-  
+
 let decomp_n_prod env sigma n = 
   let rec decrec env m ln c = if m = 0 then (ln,c) else 
     match kind_of_term (whd_betadeltaiota env sigma c) with
@@ -764,7 +770,12 @@ let decomp_sort env sigma t =
   | Sort s -> s
   | _ -> raise NotASort
 
-(* One step of approximation *)
+let is_sort env sigma arity =
+  try let _ = decomp_sort env sigma arity in true 
+  with NotASort -> false
+
+(* reduction to head-normal-form allowing delta/zeta only in argument
+   of case/fix (heuristic used by evar_conv) *)
 
 let rec apprec env sigma s =
   let (t, stack as s) = whd_betaiota_state s in
@@ -782,8 +793,6 @@ let rec apprec env sigma s =
 	     | NotReducible -> s)
     | _ -> s
 
-let hnf env sigma c = apprec env sigma (c, empty_stack)
-
 (* A reduction function like whd_betaiota but which keeps casts
  * and does not reduce redexes containing existential variables.
  * Used in Correctness.
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 78afd22b..1e9b3b5b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reductionops.mli 8812 2006-05-13 11:46:02Z herbelin $ i*)
+(*i $Id: reductionops.mli 9106 2006-09-01 11:18:17Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -37,6 +37,7 @@ and 'a stack = 'a stack_member list
 
 val empty_stack : 'a stack
 val append_stack : 'a array -> 'a stack -> 'a stack
+val append_stack_list : 'a list -> 'a stack -> 'a stack
 
 val decomp_stack : 'a stack -> ('a * 'a stack) option
 val list_of_stack : 'a stack -> 'a list
@@ -140,6 +141,7 @@ val whd_betadeltaiotaeta_stack :  stack_reduction_function
 val whd_betadeltaiotaeta_state :  state_reduction_function
 val whd_betadeltaiotaeta :  reduction_function
 
+val whd_eta : constr -> constr
 
 
 
@@ -162,6 +164,7 @@ val decomp_n_prod :
 val splay_prod_assum :
   env ->  evar_map -> constr -> Sign.rel_context * constr
 val decomp_sort : env -> evar_map -> types -> sorts
+val is_sort : env -> evar_map -> types -> bool
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
@@ -206,11 +209,8 @@ val whd_meta : (metavariable * constr) list -> constr -> constr
 val plain_instance : (metavariable * constr) list -> constr -> constr
 val instance : (metavariable * constr) list -> constr -> constr
 
-(*s Obsolete Reduction Functions *)
+(*s Heuristic for Conversion with Evar *)
 
-(*i
-val hnf : env -> 'a evar_map -> constr -> constr * constr list
-i*)
 val apprec :  state_reduction_function
 
 (*s Meta-related reduction functions *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 428a7306..ecead438 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: retyping.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
 
 open Util
 open Term
@@ -17,6 +17,7 @@ open Reductionops
 open Environ
 open Typeops
 open Declarations
+open Termops
 
 let rec subst_type env sigma typ = function
   | [] -> typ
@@ -38,6 +39,11 @@ let sort_of_atomic_type env sigma ft args =
     | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
   in concl_of_arity env ft
 
+let type_of_var env id =
+  try let (_,_,ty) = lookup_named id env in ty
+  with Not_found ->
+    anomaly ("type_of: variable "^(string_of_id id)^" unbound")
+
 let typeur sigma metamap =
   let rec type_of env cstr=
     match kind_of_term cstr with
@@ -47,18 +53,11 @@ let typeur sigma metamap =
     | Rel n ->
         let (_,_,ty) = lookup_rel n env in
         lift n ty
-    | Var id ->
-        (try
-          let (_,_,ty) = lookup_named id env in
-          body_of_type ty
-        with Not_found ->
-          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
-    | Const c ->
-        let cb = lookup_constant c env in
-        body_of_type cb.const_type
+    | Var id -> type_of_var env id
+    | Const cst -> Typeops.type_of_constant env cst
     | 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)
+    | Ind ind -> type_of_inductive env ind
+    | Construct cstr -> type_of_constructor env cstr
     | Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
@@ -73,8 +72,8 @@ let typeur sigma metamap =
          subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
-    | App(f,args) when isInd f ->
-	let t = type_of_inductive_knowing_parameters env (destInd f) args in
+    | App(f,args) when isGlobalRef f ->
+	let t = type_of_global_reference_knowing_parameters env f args in
         strip_outer_cast (subst_type env sigma t (Array.to_list args))
     | App(f,args) ->
         strip_outer_cast
@@ -97,8 +96,8 @@ let typeur sigma metamap =
 	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2)
 	  | Prop Null, (Type _ as s) -> s
 	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
-    | App(f,args) when isInd f ->
-	let t = type_of_inductive_knowing_parameters env (destInd f) args in
+    | App(f,args) when isGlobalRef f ->
+	let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
     | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | Lambda _ | Fix _ | Construct _ ->
@@ -117,18 +116,27 @@ let typeur sigma metamap =
         anomaly "sort_of: Not a type (1)"
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
-  and type_of_inductive_knowing_parameters env ind args =
-    let (_,mip) = lookup_mind_specif env ind in
+  and type_of_global_reference_knowing_parameters env c args =
     let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
-    Inductive.type_of_inductive_knowing_parameters env mip argtyps
+    match kind_of_term c with
+    | Ind ind ->
+      let (_,mip) = lookup_mind_specif env ind in
+      Inductive.type_of_inductive_knowing_parameters env mip argtyps
+    | Const cst ->
+      let t = constant_type env cst in
+      Typeops.type_of_constant_knowing_parameters env t argtyps
+    | Var id -> type_of_var env id
+    | Construct cstr -> type_of_constructor env cstr
+    | _ -> assert false
 
-  in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters
+  in type_of, sort_of, sort_family_of,
+     type_of_global_reference_knowing_parameters
 
 let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
 let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
 let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
-let type_of_inductive_knowing_parameters env sigma ind args =
-  let _,_,_,f = typeur sigma [] in f env ind args
+let type_of_global_reference_knowing_parameters env sigma c args =
+  let _,_,_,f = typeur sigma [] in f env c args
 
 let get_type_of_with_meta env sigma metamap = 
   let f,_,_,_ = typeur sigma metamap in f env
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 923123c5..733cb4b1 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: retyping.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
+(*i $Id: retyping.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -34,5 +34,6 @@ val get_assumption_of : env -> evar_map -> constr -> types
 (* Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
 
-val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> 
+val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> 
   constr array -> types
+ 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 823da969..9b8764f2 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: termops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: termops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
 
 open Pp
 open Util
@@ -855,7 +855,12 @@ let next_global_ident_away allow_secvar id avoid =
   else  
     next_global_ident_from allow_secvar (lift_ident id) avoid
 
-(* Nouvelle version de renommage des variables (DEC 98) *)
+let isGlobalRef c = 
+  match kind_of_term c with
+  | Const _ | Ind _ | Construct _ | Var _ -> true
+  | _ -> false
+
+(* nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
 
     - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
@@ -1020,3 +1025,9 @@ let rec rename_bound_var env l c =
   | Cast (c,k,t) -> mkCast (rename_bound_var env l c, k,t)
   | x -> c
 
+(* Combinators on judgments *)
+
+let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
+let on_judgment_value f j = { j with uj_val = f j.uj_val }
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
+
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 49de4838..e406b148 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: termops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: termops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
 
 open Util
 open Pp
@@ -203,3 +203,11 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t
 
 (* Test if an identifier is the basename of a global reference *)
 val is_section_variable : identifier -> bool
+
+val isGlobalRef : constr -> bool
+
+(* Combinators on judgments *)
+
+val on_judgment       : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment_type  : (types -> types) -> unsafe_judgment -> unsafe_judgment
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 78902a7d..63fdd6d5 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typing.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Util
 open Names
@@ -53,7 +53,7 @@ let rec execute env evd cstr =
         j_nf_evar (evars_of evd) (judge_of_variable env id)
 	  
     | Const c ->
-        make_judge cstr (nf_evar (evars_of evd) (constant_type env c))
+        make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c))
 	  
     | Ind ind ->
 	make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
@@ -90,12 +90,17 @@ let rec execute env evd cstr =
     | App (f,args) ->
         let jl = execute_array env evd args in
 	let j =
-	if isInd f then
-	  (* Sort-polymorphism of inductive types *)
-	  judge_of_inductive_knowing_parameters env (destInd f)
-	    (jv_nf_evar (evars_of evd) jl)
-	else
-	  execute env evd f
+	  match kind_of_term f with
+	    | Ind ind ->
+		(* Sort-polymorphism of inductive types *)
+		judge_of_inductive_knowing_parameters env ind
+		  (jv_nf_evar (evars_of evd) jl)
+	    | Const cst -> 
+		(* Sort-polymorphism of inductive types *)
+		judge_of_constant_knowing_parameters env cst
+		  (jv_nf_evar (evars_of evd) jl)
+	    | _ -> 
+		execute env evd f
 	in
 	fst (judge_of_apply env j jl)
 	    
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e4bde925..fabe24ef 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: unification.ml 9217 2006-10-05 17:31:23Z notin $ *)
 
 open Pp
 open Util
@@ -47,6 +47,16 @@ let abstract_list_all env sigma typ c l =
   with UserError _ ->
     raise (PretypeError (env,CannotGeneralize typ))
 
+(**)
+
+let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
+  match kind_of_term f with
+    | Meta k -> 
+	(k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst
+    | Evar ev ->
+      (* Currently unused: incompatible with eauto/eassumption backtracking *)
+	metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
+    | _ -> assert false
 
 (*******************************)
 
@@ -70,58 +80,77 @@ let sort_eqns = unify_r2l
 
 let unify_0 env sigma cv_pb mod_delta m n =
   let trivial_unify pb substn m n =
-    if (not(occur_meta m)) && (if mod_delta then is_fconv pb env sigma m n else eq_constr m n) then substn
+    if (not(occur_meta m)) && 
+      (if mod_delta then is_fconv pb env sigma m n else eq_constr 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
-
+  let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn =
+    let cM = Evarutil.whd_castappevar sigma curm
+    and cN = Evarutil.whd_castappevar sigma curn 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, _    -> 
+	    (* Here we check that [cN] does not contain any local variables *)
+	    if (closedn (nb_rel env) cN)
+	    then (k,cN)::metasubst,evarsubst
+	    else error_cannot_unify_local curenv sigma (curenv,m,n,cN)
+	| _, Meta k    -> 
+	    (* Here we check that [cM] does not contain any local variables *)
+	    if (closedn (nb_rel env) cM) 
+	    then (k,cM)::metasubst,evarsubst
+	    else error_cannot_unify_local curenv sigma (curenv,m,n,cM)
+	| Evar _, _ -> metasubst,((cM,cN)::evarsubst)
+	| _, Evar _ -> metasubst,((cN,cM)::evarsubst)
+	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
+	    unirec_rec (push_rel_assum (na,t1) curenv) CONV 
+	      (unirec_rec curenv CONV substn t1 t2) c1 c2
+	| Prod (na,t1,c1), Prod (_,t2,c2) ->
+	    unirec_rec (push_rel_assum (na,t1) curenv) pb 
+	      (unirec_rec curenv CONV substn t1 t2) c1 c2
+	| LetIn (_,b,_,c), _ -> unirec_rec curenv  pb substn (subst1 b c) cN
+	| _, LetIn (_,b,_,c) -> unirec_rec curenv  pb substn cM (subst1 b c)
+	    
+	| App (f1,l1), App (f2,l2) ->
+	    if
+	      isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN)
+	    then
+	      solve_pattern_eqn_array curenv f1 l1 cN substn
+	    else if
+		isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM)
+	    then
+	      solve_pattern_eqn_array curenv f2 l2 cM substn
+	    else
+	      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 curenv CONV)
+		      (unirec_rec curenv 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 curenv CONV)
+	      (unirec_rec curenv CONV 
+		  (unirec_rec curenv CONV substn p1 p2) c1 c2) cl1 cl2
+	| _ -> trivial_unify pb substn cM cN
   in
-  if (not(occur_meta m)) &&
-   (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n)
-  then 
-    ([],[])
-  else 
-    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
-    ((*sort_eqns*) mc, (*sort_eqns*) ec)
+    if (not(occur_meta m)) &&
+      (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n)
+    then 
+      ([],[])
+    else 
+      let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in
+	((*sort_eqns*) mc, (*sort_eqns*) ec)
 
 
 (* Unification
@@ -442,30 +471,30 @@ let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd =
 let w_unify allow_K env cv_pb ?(mod_delta=true) 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 cv_pb mod_delta ty1 ty2 evd
-	 with ex when precatchable_exception ex -> 
-	   try 
-	     w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
-	   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 mod_delta allow_K cv_pb ty1 ty2 evd
-	with PretypeError (env,NoOccurrenceFound c) as e -> raise e
-	  | ex when precatchable_exception ex -> 
-          try 
-	     w_typed_unify env cv_pb mod_delta ty1 ty2 evd
-          with ex when precatchable_exception ex -> 
-             error "Cannot solve a second-order unification problem")
-
-     (* General case: try first order *)
-     | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd
+    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 cv_pb mod_delta ty1 ty2 evd
+	    with ex when precatchable_exception ex -> 
+	      try 
+		w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd
+	      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 mod_delta allow_K cv_pb ty1 ty2 evd
+	    with PretypeError (env,NoOccurrenceFound c) as e -> raise e
+	      | ex when precatchable_exception ex -> 
+		  try 
+		    w_typed_unify env cv_pb mod_delta ty1 ty2 evd
+		  with ex when precatchable_exception ex -> 
+		    error "Cannot solve a second-order unification problem")
+	    
+      (* General case: try first order *)
+      | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
new file mode 100644
index 00000000..55f798de
--- /dev/null
+++ b/pretyping/vnorm.ml
@@ -0,0 +1,271 @@
+open Names
+open Declarations
+open Term
+open Environ
+open Inductive
+open Reduction 
+open Vm
+
+(*******************************************)
+(* Calcul de la forme normal d'un terme    *)
+(*******************************************)
+
+let crazy_type = mkSet 
+
+let decompose_prod env t =
+  let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
+  if name = Anonymous then (Name (id_of_string "x"),dom,codom)
+  else res
+
+exception Find_at of int
+
+(* rend le numero du constructeur correspondant au tag [tag],
+   [cst] = true si c'est un constructeur constant *)
+
+let invert_tag cst tag reloc_tbl =
+  try 
+    for j = 0 to Array.length reloc_tbl - 1 do
+      let tagj,arity = reloc_tbl.(j) in
+      if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then
+	raise (Find_at j)
+      else ()
+    done;raise Not_found 
+  with Find_at j -> (j+1)   
+             (* Argggg, ces constructeurs de ... qui commencent a 1*)
+
+let find_rectype_a env c =
+  let (t, l) = 
+    let t = whd_betadeltaiota env c in
+    try destApp t with _ -> (t,[||]) in
+  match kind_of_term t with
+  | Ind ind -> (ind, l)
+  | _ -> raise Not_found
+
+(* Instantiate inductives and parameters in constructor type *)
+let build_type_constructor mind mib params ctyp =
+  let si = ind_subst mind mib in
+  let ctyp1 = substl si ctyp in
+  let nparams = Array.length params in
+  if nparams = 0 then ctyp1
+  else
+    let _,ctyp2 = decompose_prod_n nparams ctyp1 in
+    let sp = List.rev (Array.to_list params) in substl sp ctyp2
+   
+let construct_of_constr_const env tag typ =
+  let ind,params = find_rectype env typ in
+  let (_,mip) = lookup_mind_specif env ind in
+  let i = invert_tag true tag mip.mind_reloc_tbl in
+  applistc (mkConstruct(ind,i)) params
+
+let construct_of_constr_block env tag typ =
+  let (mind,_ as ind), allargs = find_rectype_a env typ in
+  let (mib,mip) = lookup_mind_specif env ind in
+  let nparams = mib.mind_nparams in
+  let i = invert_tag false tag mip.mind_reloc_tbl in
+  let params = Array.sub allargs 0 nparams in
+  let specif = mip.mind_nf_lc in
+  let ctyp = build_type_constructor mind mib params specif.(i-1) in
+  (mkApp(mkConstruct(ind,i), params), ctyp)
+  	
+let constr_type_of_idkey env idkey =
+  match idkey with
+  | ConstKey cst ->
+      mkConst cst, Typeops.type_of_constant env cst
+  | VarKey id -> 
+      let (_,_,ty) = lookup_named id env in 
+      mkVar id, ty
+  | RelKey i -> 
+      let n = (nb_rel env - i) in
+      let (_,_,ty) = lookup_rel n env in
+      mkRel n, lift n ty
+
+let type_of_ind env ind = 
+  type_of_inductive env (Inductive.lookup_mind_specif env ind)
+
+let build_branches_type env (mind,_ as _ind) mib mip params dep p =
+  let rtbl = mip.mind_reloc_tbl in
+  (* [build_one_branch i cty] construit le type de la ieme branche (commence
+     a 0) et les lambda correspondant aux realargs *)
+  let build_one_branch i cty =
+    let typi = build_type_constructor mind mib params cty in
+    let decl,indapp = Term.decompose_prod typi in
+    let ind,cargs = find_rectype_a env indapp in
+    let nparams = Array.length params in
+    let carity = snd (rtbl.(i)) in
+    let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
+    let codom = 
+      let papp = mkApp(p,crealargs) in
+      if dep then
+	let cstr = ith_constructor_of_inductive ind (i+1) in
+        let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
+	let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in
+	mkApp(papp,[|dep_cstr|])
+      else papp
+    in 
+    decl, codom
+  in Array.mapi build_one_branch mip.mind_nf_lc
+
+let build_case_type dep p realargs c = 
+  if dep then mkApp(mkApp(p, realargs), [|c|])
+  else mkApp(p, realargs)
+
+(* La fonction de normalisation *)
+
+let rec nf_val env v t = nf_whd env (whd_val v) t 
+
+and nf_vtype env v =  nf_val env v crazy_type
+
+and nf_whd env whd typ =
+  match whd with
+  | Vsort s -> mkSort s
+  | Vprod p ->
+      let dom = nf_vtype env (dom p) in
+      let name = Name (id_of_string "x") in
+      let vc = body_of_vfun (nb_rel env) (codom p) in
+      let codom = nf_vtype (push_rel (name,None,dom) env) vc  in      
+      mkProd(name,dom,codom)	  
+  | Vfun f -> nf_fun env f typ
+  | Vfix(f,None) -> nf_fix env f
+  | Vfix(f,Some vargs) -> fst (nf_fix_app env f vargs)
+  | Vcofix(cf,_,None) -> nf_cofix env cf 
+  | Vcofix(cf,_,Some vargs) -> 
+      let cfd = nf_cofix env cf in
+      let i,(_,ta,_) = destCoFix cfd in
+      let t = ta.(i) in
+      let _, args = nf_args env vargs t in
+      mkApp(cfd,args) 
+  | Vconstr_const n -> construct_of_constr_const env n typ
+  | Vconstr_block b ->
+      let capp,ctyp = construct_of_constr_block env (btag b) typ in
+      let args = nf_bargs env b ctyp in
+      mkApp(capp,args)
+  | Vatom_stk(Aid idkey, stk) ->
+      let c,typ = constr_type_of_idkey env idkey in
+      nf_stk env c typ stk
+  | Vatom_stk(Aiddef(idkey,v), stk) ->
+      nf_whd env (whd_stack v stk) typ
+  | Vatom_stk(Aind ind, stk) ->
+      nf_stk env (mkInd ind) (type_of_ind env ind) stk 
+	
+and nf_stk env c t stk  =
+  match stk with
+  | [] -> c
+  | Zapp vargs :: stk ->
+      let t, args = nf_args env vargs t in
+      nf_stk env (mkApp(c,args)) t stk 
+  | Zfix (f,vargs) :: stk ->  
+      let fa, typ = nf_fix_app env f vargs in
+      let _,_,codom = decompose_prod env typ in
+      nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
+  | Zswitch sw :: stk -> 
+      let (mind,_ as ind),allargs = find_rectype_a env t in
+      let (mib,mip) = Inductive.lookup_mind_specif env ind in
+      let nparams = mib.mind_nparams in
+      let params,realargs = Util.array_chop nparams allargs in
+      let pT = 
+	hnf_prod_applist env (type_of_ind env ind) (Array.to_list params) in
+      let dep, p = nf_predicate env ind mip params (type_of_switch sw) pT in
+      (* Calcul du type des branches *)
+      let btypes = build_branches_type env ind mib mip params dep p in
+      (* calcul des branches *)
+      let bsw = branch_of_switch (nb_rel env) sw in
+      let mkbranch i (n,v) =
+	let decl,codom = btypes.(i) in
+	let env = 
+	  List.fold_right 
+	    (fun (name,t) env -> push_rel (name,None,t) env) decl env in
+	let b = nf_val env v codom in
+	compose_lam decl b 
+      in 
+      let branchs = Array.mapi mkbranch bsw in
+      let tcase = build_case_type dep p realargs c in
+      let ci = case_info sw in
+      nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+
+and nf_predicate env ind mip params v pT =
+  match whd_val v, kind_of_term pT with
+  | Vfun f, Prod _ ->
+      let k = nb_rel env in
+      let vb = body_of_vfun k f in
+      let name,dom,codom = decompose_prod env pT in
+      let dep,body = 
+	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
+      dep, mkLambda(name,dom,body)
+  | Vfun f, _ -> 
+      let k = nb_rel env in
+      let vb = body_of_vfun k f in
+      let name = Name (id_of_string "c") in
+      let n = mip.mind_nrealargs in
+      let rargs = Array.init n (fun i -> mkRel (n-i)) in
+      let dom = mkApp(mkApp(mkInd ind,params),rargs) in
+      let body = nf_vtype (push_rel (name,None,dom) env) vb in
+      true, mkLambda(name,dom,body)
+  | _, _ -> false, nf_val env v crazy_type
+	
+and nf_args env vargs t =
+  let t = ref t in
+  let len = nargs vargs in
+  let args = 
+    Array.init len 
+      (fun i ->
+	let _,dom,codom = decompose_prod env !t in
+	let c = nf_val env (arg vargs i) dom in
+	t := subst1 c codom; c) in
+  !t,args
+
+and nf_bargs env b t =
+  let t = ref t in
+  let len = bsize b in
+  let args =
+    Array.init len 
+      (fun i -> 
+	let _,dom,codom = decompose_prod env !t in
+	let c = nf_val env (bfield b i) dom in
+	t := subst1 c codom; c) in
+  args
+
+and nf_fun env f typ =
+  let k = nb_rel env in
+  let vb = body_of_vfun k f in
+  let name,dom,codom = decompose_prod env typ in
+  let body = nf_val (push_rel (name,None,dom) env) vb codom in
+  mkLambda(name,dom,body)
+
+and nf_fix env f =
+  let init = current_fix f in
+  let rec_args = rec_args f in
+  let k = nb_rel env in
+  let vb, vt = reduce_fix k f in
+  let ndef = Array.length vt in
+  let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
+  let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in
+  let env = push_rec_types (name,ft,ft) env in 
+  let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in
+  mkFix ((rec_args,init),(name,ft,fb))
+      
+and nf_fix_app env f vargs =
+  let fd = nf_fix env f in
+  let (_,i),(_,ta,_) = destFix fd in
+  let t = ta.(i) in
+  let t, args = nf_args env vargs t in
+  mkApp(fd,args),t
+  
+and nf_cofix env cf =
+  let init = current_cofix cf in
+  let k = nb_rel env in
+  let vb,vt = reduce_cofix k cf in
+  let ndef = Array.length vt in
+  let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
+  let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in
+  let env = push_rec_types (name,cft,cft) env in 
+  let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in
+  mkCoFix (init,(name,cft,cfb))
+  
+let cbv_vm env c t  =
+  let transp = transp_values () in
+  if not transp then set_transp_values true; 
+  let v = Vconv.val_of_constr env c in
+  let c = nf_val env v t in
+  if not transp then set_transp_values false; 
+  c
+  
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
new file mode 100644
index 00000000..2ea94bfb
--- /dev/null
+++ b/pretyping/vnorm.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  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*)
+open Names
+open Term
+open Environ
+open Reduction
+(*i*)
+
+(*s Reduction functions *)
+val cbv_vm : env -> constr -> types -> constr
+