Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 503 insertions, 261 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7aa2272d..e6fa6eec 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Pp
 open Util
 open Names
@@ -20,8 +18,7 @@ open Environ
 open Evd
 open Reduction
 open Reductionops
-open Rawterm
-open Pattern
+open Glob_term
 open Evarutil
 open Pretype_errors
 open Retyping
@@ -51,7 +48,7 @@ let abstract_scheme env c l lname_typ =
    are unclear...
        if occur_meta ta then error "cannot find a type for the generalisation"
        else *) if occur_meta a then mkLambda_name env (na,ta,t)
-       else mkLambda_name env (na,ta,subst_term_occ locc a t))
+       else mkLambda_name env (na,ta,subst_closed_term_occ locc a t))
     c
     (List.rev l)
     lname_typ
@@ -66,6 +63,19 @@ let abstract_list_all env evd typ c l =
   with UserError _ | Type_errors.TypeError _ ->
     error_cannot_find_well_typed_abstraction env evd p l
 
+let set_occurrences_of_last_arg args =
+  Some all_occurrences :: List.tl (array_map_to_list (fun _ -> None) args)
+
+let abstract_list_all_with_dependencies env evd typ c l =
+  let evd,ev = new_evar evd env typ in
+  let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in
+  let argoccs = set_occurrences_of_last_arg (snd ev') in
+  let evd,b =
+    Evarconv.second_order_matching empty_transparent_state
+      env evd ev' argoccs c in
+  if b then nf_evar evd (existential_value evd (destEvar ev))
+  else error "Cannot find a well-typed abstraction."
+
 (**)
 
 (* A refinement of [conv_pb]: the integers tells how many arguments
@@ -73,23 +83,16 @@ let abstract_list_all env evd typ c l =
    is non zero, steps of eta-expansion will be allowed
 *)
 
-type conv_pb_up_to_eta = Cumul | ConvUnderApp of int * int
-
-let topconv = ConvUnderApp (0,0)
-let of_conv_pb = function CONV -> topconv | CUMUL -> Cumul
-let conv_pb_of = function ConvUnderApp _ -> CONV | Cumul -> CUMUL
-let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb
-
 let opp_status = function
   | IsSuperType -> IsSubType
   | IsSubType -> IsSuperType
-  | ConvUpToEta _ | UserGiven as x -> x
+  | Conv -> Conv
 
 let add_type_status (x,y) = ((x,TypeNotProcessed),(y,TypeNotProcessed))
 
 let extract_instance_status = function
-  | Cumul -> add_type_status (IsSubType, IsSuperType)
-  | ConvUnderApp (n1,n2) -> add_type_status (ConvUpToEta n1, ConvUpToEta n2)
+  | CUMUL -> add_type_status (IsSubType, IsSuperType)
+  | CONV -> add_type_status (Conv, Conv)
 
 let rec assoc_pair x = function
     [] -> raise Not_found
@@ -110,7 +113,7 @@ let pose_all_metas_as_evars env evd t =
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = if mvs = Evd.Metaset.empty then ty else aux ty in
         let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in
-        evdref := meta_assign mv (ev,(ConvUpToEta 0,TypeNotProcessed)) !evdref;
+        evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
         ev)
   | _ ->
       map_constr aux t in
@@ -121,15 +124,15 @@ let pose_all_metas_as_evars env evd t =
 let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) =
   match kind_of_term f with
     | Meta k ->
-	let c = solve_pattern_eqn env (Array.to_list l) c in
-	let n = Array.length l - List.length (fst (decompose_lam c)) in
-	let pb = (ConvUpToEta n,TypeNotProcessed) in
+	let sigma,c = pose_all_metas_as_evars env sigma c in
+	let c = solve_pattern_eqn env l c in
+	let pb = (Conv,TypeNotProcessed) in
 	  if noccur_between 1 nb c then
             sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst
-	  else error_cannot_unify_local env sigma (mkApp (f, l),c,c)
+	  else error_cannot_unify_local env sigma (applist (f, l),c,c)
     | Evar ev ->
 	let sigma,c = pose_all_metas_as_evars env sigma c in
-	sigma,metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
+	sigma,metasubst,(env,ev,solve_pattern_eqn env l c)::evarsubst
     | _ -> assert false
 
 let push d (env,n) = (push_rel_assum d env,n+1)
@@ -161,46 +164,172 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
       optread  = (fun () -> !global_evars_pattern_unification_flag);
       optwrite = (:=) global_evars_pattern_unification_flag }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "pattern-unification for existential variables in tactics";
+      optkey   = ["Tactic";"Pattern";"Unification"];
+      optread  = (fun () -> !global_evars_pattern_unification_flag);
+      optwrite = (:=) global_evars_pattern_unification_flag }
+
 type unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
-  use_metas_eagerly : bool;
+    (* What this flag controls was activated with all constants transparent, *)
+    (* even for auto, since Coq V5.10 *)
+
+  use_metas_eagerly_in_conv_on_closed_terms : bool;
+    (* This refinement of the conversion on closed terms is activable *)
+    (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *)
+
   modulo_delta : Names.transparent_state;
+    (* This controls which constant are unfoldable; this is on for apply *)
+    (* (but not simple apply) since Feb 2008 for 8.2 *)
+
+  modulo_delta_types : Names.transparent_state;
+
+  check_applied_meta_types : bool;
+    (* This controls whether meta's applied to arguments have their *)
+    (* type unified with the type of their instance *)
+
   resolve_evars : bool;
-  use_evars_pattern_unification : bool
+    (* This says if type classes instances resolution must be used to infer *)
+    (* the remaining evars *)
+
+  use_pattern_unification : bool;
+    (* This says if type classes instances resolution must be used to infer *)
+    (* the remaining evars *)
+
+  use_meta_bound_pattern_unification : bool;
+    (* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *)
+    (* This allows for instance to unify "forall x:A, B(x)" with "A' -> B'" *)
+    (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *)
+
+  frozen_evars : ExistentialSet.t;
+    (* Evars of this set are considered axioms and never instantiated *)
+    (* Useful e.g. for autorewrite *)
+
+  restrict_conv_on_strict_subterms : bool;
+    (* No conversion at the root of the term; potentially useful for rewrite *)
+
+  modulo_betaiota : bool;
+    (* Support betaiota in the reduction *)
+    (* Note that zeta is always used *)
+
+  modulo_eta : bool;
+    (* Support eta in the reduction *)
+
+  allow_K_in_toplevel_higher_order_unification : bool
+    (* This is used only in second/higher order unification when looking for *)
+    (* subterms (rewrite and elim) *)
 }
 
+(* Default flag for unifying a type against a type (e.g. apply) *)
+(* We set all conversion flags *)
 let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = full_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = true;
   resolve_evars = false;
-  use_evars_pattern_unification = true;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = true;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
+      (* in fact useless when not used in w_unify_to_subterm_list *)
 }
 
+(* Default flag for the "simple apply" version of unification of a *)
+(* type against a type (e.g. apply) *)
+(* We set only the flags available at the time the new "apply" extends *)
+(* out of "simple apply" *)
 let default_no_delta_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
+  modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = false;
+  resolve_evars = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false;
+  modulo_betaiota = false;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
+}
+
+(* Default flags for looking for subterms in elimination tactics *)
+(* Not used in practice at the current date, to the exception of *)
+(* allow_K) because only closed terms are involved in *)
+(* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
+(* call w_unify for induction/destruct/case/elim  (13/6/2011) *)
+let elim_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
+  modulo_delta = full_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = true;
+  resolve_evars = false;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false; (* ? *)
+  modulo_betaiota = false;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = true
+}
+
+let elim_no_delta_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
   modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  check_applied_meta_types = false;
   resolve_evars = false;
-  use_evars_pattern_unification = false;
+  use_pattern_unification = false;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = ExistentialSet.empty;
+  restrict_conv_on_strict_subterms = false; (* ? *)
+  modulo_betaiota = false;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = true
 }
 
+let set_no_head_reduction flags =
+  { flags with restrict_conv_on_strict_subterms = true }
+
 let use_evars_pattern_unification flags =
-  !global_evars_pattern_unification_flag && flags.use_evars_pattern_unification
+  !global_evars_pattern_unification_flag && flags.use_pattern_unification
   && Flags.version_strictly_greater Flags.V8_2
 
+let use_metas_pattern_unification flags nb l =
+  !global_evars_pattern_unification_flag && flags.use_pattern_unification
+  || (Flags.version_less_or_equal Flags.V8_3 || 
+      flags.use_meta_bound_pattern_unification) &&
+     array_for_all (fun c -> isRel c && destRel c <= nb) l
+
 let expand_key env = function
   | Some (ConstKey cst) -> constant_opt_value env cst
   | Some (VarKey id) -> (try named_body id env with Not_found -> None)
   | Some (RelKey _) -> None
   | None -> None
 
-let key_of flags f =
+let subterm_restriction is_subterm flags =
+  not is_subterm && flags.restrict_conv_on_strict_subterms
+
+let key_of b flags f =
+  if subterm_restriction b flags then None else
   match kind_of_term f with
   | Const cst when is_transparent (ConstKey cst) &&
         Cpred.mem cst (snd flags.modulo_delta) ->
@@ -219,20 +348,51 @@ let oracle_order env cf1 cf2 =
   | Some k1 ->
       match cf2 with
       | None -> Some true
-      | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
+      | Some k2 -> Some (Conv_oracle.oracle_order false k1 k2)
+
+let do_reduce ts (env, nb) sigma c =
+  let (t, stack') = whd_betaiota_deltazeta_for_iota_state ts env sigma (c, empty_stack) in
+  let l = list_of_stack stack' in
+    applist (t, l)
+
+let use_full_betaiota flags =
+  flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
+
+let isAllowedEvar flags c = match kind_of_term c with
+  | Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars)
+  | _ -> false
+
+let check_compatibility env (sigma,metasubst,evarsubst) tyM tyN =
+  match subst_defined_metas metasubst tyM with
+  | None -> ()
+  | Some m ->
+  match subst_defined_metas metasubst tyN with
+  | None -> ()
+  | Some n ->
+      if not (is_trans_fconv CONV full_transparent_state env sigma m n)
+         && is_ground_term sigma m && is_ground_term sigma n
+      then
+	error_cannot_unify env sigma (m,n)
 
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
-  let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
+  let rec unirec_rec (curenv,nb as curenvnb) pb b wt ((sigma,metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_head_evar sigma curm
     and cN = Evarutil.whd_head_evar sigma curn in
       match (kind_of_term cM,kind_of_term cN) with
 	| Meta k1, Meta k2 ->
+            if k1 = k2 then substn else
 	    let stM,stN = extract_instance_status pb in
-	    if k2 < k1
-	    then sigma,(k1,cN,stN)::metasubst,evarsubst
-	    else if k1 = k2 then substn
+            if wt && flags.check_applied_meta_types then
+              (let tyM = Typing.meta_type sigma k1 in
+               let tyN = Typing.meta_type sigma k2 in
+               check_compatibility curenv substn tyM tyN);
+	    if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
 	    else sigma,(k2,cM,stM)::metasubst,evarsubst
 	| Meta k, _ when not (dependent cM cN) ->
+            if wt && flags.check_applied_meta_types then
+              (let tyM = Typing.meta_type sigma k in
+               let tyN = get_type_of curenv sigma cN in
+               check_compatibility curenv substn tyM tyN);
 	    (* Here we check that [cN] does not contain any local variables *)
 	    if nb = 0 then
               sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
@@ -242,6 +402,10 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Meta k when not (dependent cN cM) ->
+            if wt && flags.check_applied_meta_types then
+              (let tyM = get_type_of curenv sigma cM in
+               let tyN = Typing.meta_type sigma k in
+               check_compatibility curenv substn tyM tyN);
 	    (* Here we check that [cM] does not contain any local variables *)
 	    if nb = 0 then
               (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst)
@@ -250,65 +414,123 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
               (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
-	| Evar ev, _ -> sigma,metasubst,((ev,cN)::evarsubst)
-	| _, Evar ev -> sigma,metasubst,((ev,cM)::evarsubst)
+	| Evar (evk,_ as ev), _
+            when not (ExistentialSet.mem evk flags.frozen_evars) ->
+	    let cmvars = free_rels cM and cnvars = free_rels cN in
+	      if Intset.subset cnvars cmvars then
+		sigma,metasubst,((curenv,ev,cN)::evarsubst)
+	      else error_cannot_unify_local curenv sigma (m,n,cN)
+	| _, Evar (evk,_ as ev)
+            when not (ExistentialSet.mem evk flags.frozen_evars) ->
+	    let cmvars = free_rels cM and cnvars = free_rels cN in
+	      if Intset.subset cmvars cnvars then
+		sigma,metasubst,((curenv,ev,cM)::evarsubst)
+	      else error_cannot_unify_local curenv sigma (m,n,cN)
+	| Sort s1, Sort s2 ->
+	    (try 
+	       let sigma' = 
+		 if cv_pb = CUMUL 
+		 then Evd.set_leq_sort sigma s1 s2 
+		 else Evd.set_eq_sort sigma s1 s2 
+	       in (sigma', metasubst, evarsubst)
+	     with _ -> error_cannot_unify curenv sigma (m,n))
+	      
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
-	    unirec_rec (push (na,t1) curenvnb) topconv true
-	      (unirec_rec curenvnb topconv true substn t1 t2) c1 c2
+	    unirec_rec (push (na,t1) curenvnb) CONV true wt
+	      (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2
 	| Prod (na,t1,c1), Prod (_,t2,c2) ->
-	    unirec_rec (push (na,t1) curenvnb) (prod_pb pb) true
-	      (unirec_rec curenvnb topconv true substn t1 t2) c1 c2
-	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b substn (subst1 a c) cN
-	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b substn cM (subst1 a c)
+	    unirec_rec (push (na,t1) curenvnb) pb true false
+	      (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2
+	| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b wt substn (subst1 a c) cN
+	| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b wt substn cM (subst1 a c)
+
+        (* eta-expansion *)
+	| Lambda (na,t1,c1), _ when flags.modulo_eta ->
+	    unirec_rec (push (na,t1) curenvnb) CONV true wt substn
+	      c1 (mkApp (lift 1 cN,[|mkRel 1|]))
+	| _, Lambda (na,t2,c2) when flags.modulo_eta ->
+	    unirec_rec (push (na,t2) curenvnb) CONV true wt substn
+	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
-            array_fold_left2 (unirec_rec curenvnb topconv true)
-	      (unirec_rec curenvnb topconv true
-		  (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
-
-	| App (f1,l1), _ when
-	    (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) &
-	    is_unification_pattern curenvnb f1 l1 cN &
-	    not (dependent f1 cN) ->
-	      solve_pattern_eqn_array curenvnb f1 l1 cN substn
+            (try 
+	       array_fold_left2 (unirec_rec curenvnb CONV true wt)
+		 (unirec_rec curenvnb CONV true false
+		    (unirec_rec curenvnb CONV true false substn p1 p2) c1 c2)
+                 cl1 cl2
+	     with ex when precatchable_exception ex ->
+	       reduce curenvnb pb b wt substn cM cN)
+
+	| App (f1,l1), _ when 
+	    (isMeta f1 && use_metas_pattern_unification flags nb l1
+            || use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
+            (match
+                is_unification_pattern curenvnb sigma f1 (Array.to_list l1) cN
+             with
+             | None ->
+                 (match kind_of_term cN with
+                 | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
+                 | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)
+             | Some l ->
+                 solve_pattern_eqn_array curenvnb f1 l cN substn)
 
 	| _, App (f2,l2) when
-	    (isMeta f2 || use_evars_pattern_unification flags && isEvar f2) &
-	    is_unification_pattern curenvnb f2 l2 cM &
-	    not (dependent f2 cM) ->
-	      solve_pattern_eqn_array curenvnb f2 l2 cM substn
+	    (isMeta f2 && use_metas_pattern_unification flags nb l2
+            || use_evars_pattern_unification flags && isAllowedEvar flags f2) ->
+            (match
+                is_unification_pattern curenvnb sigma f2 (Array.to_list l2) cM
+             with
+             | None ->
+                 (match kind_of_term cM with
+                 | App (f1,l1) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
+                 | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)
+             | Some l ->
+	         solve_pattern_eqn_array curenvnb f2 l cM substn)
 
 	| App (f1,l1), App (f2,l2) ->
-	    let len1 = Array.length l1
-	    and len2 = Array.length l2 in
-	      (try
-		  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
-		  let pb = ConvUnderApp (len1,len2) in
-		  array_fold_left2 (unirec_rec curenvnb topconv true)
-		    (unirec_rec curenvnb pb true substn f1 f2) l1 l2
-		with ex when precatchable_exception ex ->
-		  try expand curenvnb pb b substn cM f1 l1 cN f2 l2
-		  with ex when precatchable_exception ex ->
-		    canonical_projections curenvnb pb b cM cN substn)
+            unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
 
 	| _ ->
-	    try canonical_projections curenvnb pb b cM cN substn
-	    with ex when precatchable_exception ex ->
-              if constr_cmp (conv_pb_of cv_pb) cM cN then substn else
-		let (f1,l1) =
-		  match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
-		let (f2,l2) =
-		  match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
-		  expand curenvnb pb b substn cM f1 l1 cN f2 l2
+            unify_not_same_head curenvnb pb b wt substn cM cN
 
-  and expand (curenv,_ as curenvnb) pb b (sigma,metasubst,_ as substn) cM f1 l1 cN f2 l2 =
+  and unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 =
+    try
+      let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
+      array_fold_left2 (unirec_rec curenvnb CONV true false)
+	(unirec_rec curenvnb CONV true true substn f1 f2) l1 l2
+    with ex when precatchable_exception ex ->
+    try reduce curenvnb pb b false substn cM cN
+    with ex when precatchable_exception ex ->
+    try expand curenvnb pb b false substn cM f1 l1 cN f2 l2
+    with ex when precatchable_exception ex ->
+    canonical_projections curenvnb pb b cM cN substn
+
+  and unify_not_same_head curenvnb pb b wt substn cM cN =
+    try canonical_projections curenvnb pb b cM cN substn
+    with ex when precatchable_exception ex ->
+    if constr_cmp cv_pb cM cN then substn else
+    try reduce curenvnb pb b wt substn cM cN
+    with ex when precatchable_exception ex ->
+    let (f1,l1) =
+      match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
+    let (f2,l2) =
+      match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
+    expand curenvnb pb b wt substn cM f1 l1 cN f2 l2
+
+  and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN =
+    if use_full_betaiota flags && not (subterm_restriction b flags) then
+      let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
+	if not (eq_constr cM cM') then
+	  unirec_rec curenvnb pb b wt substn cM' cN
+	else
+	  let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
+	    if not (eq_constr cN cN') then
+	      unirec_rec curenvnb pb b wt substn cM cN'
+	    else error_cannot_unify (fst curenvnb) sigma (cM,cN)
+    else
+      error_cannot_unify (fst curenvnb) sigma (cM,cN)
+	    
+  and expand (curenv,_ as curenvnb) pb b wt (sigma,metasubst,_ as substn) cM f1 l1 cN f2 l2 =
 
     if
       (* Try full conversion on meta-free terms. *)
@@ -323,17 +545,19 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	 (it is used by apply and rewrite); it might now be redundant
 	 with the support for delta-expansion (which is used
 	 essentially for apply)... *)
+      not (subterm_restriction b flags) &&
       match flags.modulo_conv_on_closed_terms with
       | None -> false
       | Some convflags ->
-      let subst = if flags.use_metas_eagerly then metasubst else ms in
+      let subst = if flags.use_metas_eagerly_in_conv_on_closed_terms then metasubst else ms in
       match subst_defined_metas subst cM with
       | None -> (* some undefined Metas in cM *) false
       | Some m1 ->
       match subst_defined_metas subst cN with
       | None -> (* some undefined Metas in cN *) false
       | Some n1 ->
-	  if is_trans_fconv (conv_pb_of pb) convflags env sigma m1 n1
+          (* No subterm restriction there, too much incompatibilities *)
+	  if is_trans_fconv pb convflags env sigma m1 n1
 	  then true else
 	    if is_ground_term sigma m1 && is_ground_term sigma n1 then
 	      error_cannot_unify curenv sigma (cM,cN)
@@ -341,55 +565,52 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
     then
       substn
     else
-      if b then
-      (* Try delta-expansion if in subterms or if asked to conv at top *)
-      let cf1 = key_of flags f1 and cf2 = key_of flags f2 in
+      let cf1 = key_of b flags f1 and cf2 = key_of b flags f2 in
 	match oracle_order curenv cf1 cf2 with
 	| None -> error_cannot_unify curenv sigma (cM,cN)
 	| Some true ->
 	    (match expand_key curenv cf1 with
 	    | Some c ->
-		unirec_rec curenvnb pb b substn
+		unirec_rec curenvnb pb b wt substn
                   (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 	    | None ->
 		(match expand_key curenv cf2 with
 		| Some c ->
-		    unirec_rec curenvnb pb b substn cM
+		    unirec_rec curenvnb pb b wt substn cM
                       (whd_betaiotazeta sigma (mkApp(c,l2)))
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 	| Some false ->
 	    (match expand_key curenv cf2 with
 	    | Some c ->
-		unirec_rec curenvnb pb b substn cM
+		unirec_rec curenvnb pb b wt substn cM
                   (whd_betaiotazeta sigma (mkApp(c,l2)))
 	    | None ->
 		(match expand_key curenv cf1 with
 		| Some c ->
-		    unirec_rec curenvnb pb b substn
+		    unirec_rec curenvnb pb b wt substn
                       (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
-    else
-      error_cannot_unify curenv sigma (cM,cN)
 
   and canonical_projections curenvnb pb b cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp cM then
 	let f1l1 = decompose_app cM in
-	  if is_open_canonical_projection sigma f1l1 then
+	  if is_open_canonical_projection env sigma f1l1 then
 	    let f2l2 = decompose_app cN in
 	      solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
-      if flags.modulo_conv_on_closed_terms = None then
+      if flags.modulo_conv_on_closed_terms = None ||
+         subterm_restriction b flags then
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else
 	try f1 () with e when precatchable_exception e ->
 	  if isApp cN then
 	    let f2l2 = decompose_app cN in
-	      if is_open_canonical_projection sigma f2l2 then
+	      if is_open_canonical_projection env sigma f2l2 then
 		let f1l1 = decompose_app cM in
 		  solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn
 	      else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -413,20 +634,20 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       try List.fold_left2 f substn l l'
       with Invalid_argument "List.fold_left2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
-    let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b s u1 (substl ks u))
+    let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
       (evd,ms,es) us2 us in
-    let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b s u1 (substl ks u))
+    let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
       substn params1 params in
-    let substn = unilist2 (unirec_rec curenvnb pb b) substn ts ts1 in
-      unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
+    let substn = unilist2 (unirec_rec curenvnb pb b false) substn ts ts1 in
+      unirec_rec curenvnb pb b false substn c1 (applist (c,(List.rev ks)))
 
   in
-  let evd = create_evar_defs sigma in
-    if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n then false 
+  let evd = sigma in
+    if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n
+        || subterm_restriction conv_at_top flags then false
       else if (match flags.modulo_conv_on_closed_terms with
-      | Some flags ->
-	  is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
-      | None -> constr_cmp (conv_pb_of cv_pb) m n) then true 
+      | Some convflags -> is_trans_fconv cv_pb convflags env sigma m n
+      | _ -> constr_cmp cv_pb m n) then true
       else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
             | Some (cv_id, cv_k), (dl_id, dl_k) ->
                 Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
@@ -434,74 +655,67 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
                 Idpred.is_empty dl_id && Cpred.is_empty dl_k)
       then error_cannot_unify env sigma (m, n) else false)
     then subst
-    else unirec_rec (env,0) cv_pb conv_at_top subst m n
+    else unirec_rec (env,0) cv_pb conv_at_top false subst m n
 
 let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
 
 let left = true
 let right = false
 
-let pop k = if k=0 then 0 else k-1
-
-let rec unify_with_eta keptside flags env sigma k1 k2 c1 c2 =
-  (* Reason up to limited eta-expansion: ci is allowed to start with ki lam *)
-  (* Question: try whd_betadeltaiota on ci if ki>0 ? *)
+let rec unify_with_eta keptside flags env sigma c1 c2 =
+(* Question: try whd_betadeltaiota on ci if not two lambdas? *)
   match kind_of_term c1, kind_of_term c2 with
   | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) ->
-      let env' = push_rel_assum (na,t1) env in
-      let sigma,metas,evars = unify_0 env sigma topconv flags t1 t2 in
-      let side,status,(sigma,metas',evars') =
-	unify_with_eta keptside flags env' sigma (pop k1) (pop k2) c1' c2'
-      in (side,status,(sigma,metas@metas',evars@evars'))
-  | (Lambda (na,t,c1'),_) when k2 > 0 ->
-      let env' = push_rel_assum (na,t) env in
-      let side = left in (* expansion on the right: we keep the left side *)
-      unify_with_eta side flags env' sigma (pop k1) (k2-1)
-	c1' (mkApp (lift 1 c2,[|mkRel 1|]))
-  | (_,Lambda (na,t,c2')) when k1 > 0 ->
-      let env' = push_rel_assum (na,t) env in
-      let side = right in (* expansion on the left: we keep the right side *)
-      unify_with_eta side flags env' sigma (k1-1) (pop k2)
-	(mkApp (lift 1 c1,[|mkRel 1|])) c2'
+    let env' = push_rel_assum (na,t1) env in
+    let sigma,metas,evars = unify_0 env sigma CONV flags t1 t2 in
+    let side,(sigma,metas',evars') =
+      unify_with_eta keptside flags env' sigma c1' c2'
+    in (side,(sigma,metas@metas',evars@evars'))
+  | (Lambda (na,t,c1'),_)->
+    let env' = push_rel_assum (na,t) env in
+    let side = left in (* expansion on the right: we keep the left side *)
+      unify_with_eta side flags env' sigma
+      c1' (mkApp (lift 1 c2,[|mkRel 1|]))
+  | (_,Lambda (na,t,c2')) ->
+    let env' = push_rel_assum (na,t) env in
+    let side = right in (* expansion on the left: we keep the right side *)
+      unify_with_eta side flags env' sigma
+      (mkApp (lift 1 c1,[|mkRel 1|])) c2'
   | _ ->
-      (keptside,ConvUpToEta(min k1 k2),
-       unify_0 env sigma topconv flags c1 c2)
-
+    (keptside,unify_0 env sigma CONV flags c1 c2)
+    
 (* We solved problems [?n =_pb u] (i.e. [u =_(opp pb) ?n]) and [?n =_pb' u'],
    we now compute the problem on [u =? u'] and decide which of u or u' is kept
 
    Rem: the upper constraint is lost in case u <= ?n <= u' (and symmetrically
    in the case u' <= ?n <= u)
  *)
-
+    
 let merge_instances env sigma flags st1 st2 c1 c2 =
   match (opp_status st1, st2) with
-  | (UserGiven, ConvUpToEta n2) ->
-      unify_with_eta left flags env sigma 0 n2 c1 c2
-  | (ConvUpToEta n1, UserGiven) ->
-      unify_with_eta right flags env sigma n1 0 c1 c2
-  | (ConvUpToEta n1, ConvUpToEta n2) ->
+  | (Conv, Conv) ->
       let side = left (* arbitrary choice, but agrees with compatibility *) in
-      unify_with_eta side flags env sigma n1 n2 c1 c2
-  | ((IsSubType | ConvUpToEta _ | UserGiven as oppst1),
-     (IsSubType | ConvUpToEta _ | UserGiven)) ->
-      let res = unify_0 env sigma Cumul flags c2 c1 in
+      let (side,res) = unify_with_eta side flags env sigma c1 c2 in
+      (side,Conv,res)
+  | ((IsSubType | Conv as oppst1),
+     (IsSubType | Conv)) ->
+    let res = unify_0 env sigma CUMUL flags c2 c1 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
-      else if st2=IsSubType or st1=UserGiven then (left, st1, res)
+      else if st2=IsSubType then (left, st1, res)
       else (right, st2, res)
-  | ((IsSuperType | ConvUpToEta _ | UserGiven as oppst1),
-     (IsSuperType | ConvUpToEta _ | UserGiven)) ->
-      let res = unify_0 env sigma Cumul flags c1 c2 in
+  | ((IsSuperType | Conv as oppst1),
+     (IsSuperType | Conv)) ->
+    let res = unify_0 env sigma CUMUL flags c1 c2 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
-      else if st2=IsSuperType or st1=UserGiven then (left, st1, res)
+      else if st2=IsSuperType then (left, st1, res)
       else (right, st2, res)
   | (IsSuperType,IsSubType) ->
-      (try (left, IsSubType, unify_0 env sigma Cumul flags c2 c1)
-       with _ -> (right, IsSubType, unify_0 env sigma Cumul flags c1 c2))
+    (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
+     with _ -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
   | (IsSubType,IsSuperType) ->
-      (try (left, IsSuperType, unify_0 env sigma Cumul flags c1 c2)
-       with _ -> (right, IsSuperType, unify_0 env sigma Cumul flags c2 c1))
-
+    (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
+     with _ -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
+    
 (* Unification
  *
  * Procedure:
@@ -557,18 +771,20 @@ let applyHead env evd n c  =
       (evd, c)
     else
       match kind_of_term (whd_betadeltaiota env evd cty) with
-        | Prod (_,c1,c2) ->
-            let (evd',evar) =
-	      Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
-	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
-	| _ -> error "Apply_Head_Then"
+      | Prod (_,c1,c2) ->
+        let (evd',evar) =
+	  Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
+	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
+      | _ -> error "Apply_Head_Then"
   in
-  apprec n c (Typing.type_of env evd c) evd
-
-let is_mimick_head f =
+    apprec n c (Typing.type_of env evd c) evd
+    
+let is_mimick_head ts f =
   match kind_of_term f with
-      (Const _|Var _|Rel _|Construct _|Ind _) -> true
-    | _ -> false
+  | Const c -> not (Closure.is_transparent_constant ts c)
+  | Var id -> not (Closure.is_transparent_variable ts id)
+  | (Rel _|Construct _|Ind _) -> true
+  | _ -> false
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
@@ -580,14 +796,14 @@ let try_to_coerce env evd c cty tycon =
 let w_coerce_to_type env evd c cty mvty =
   let evd,mvty = pose_all_metas_as_evars env evd mvty in
   let tycon = mk_tycon_type mvty in
-  try try_to_coerce env evd c cty tycon
-  with e when precatchable_exception e ->
+    try try_to_coerce env evd c cty tycon
+    with e when precatchable_exception e ->
     (* inh_conv_coerce_rigid_to should have reasoned modulo reduction
        but there are cases where it though it was not rigid (like in
        fst (nat,nat)) and stops while it could have seen that it is rigid *)
     let cty = Tacred.hnf_constr env evd cty in
-    try_to_coerce env evd c cty tycon
-
+      try_to_coerce env evd c cty tycon
+	  
 let w_coerce env evd mv c =
   let cty = get_type_of env evd c in
   let mvty = Typing.meta_type evd mv in
@@ -596,25 +812,17 @@ let w_coerce env evd mv c =
 let unify_to_type env sigma flags c status u =
   let c = refresh_universes c in
   let t = get_type_of env sigma c in
-  let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in
-  let u = Tacred.hnf_constr env sigma u in
-    try
-      if status = IsSuperType then
-	unify_0 env sigma Cumul flags u t
-      else if status = IsSubType then
-	unify_0 env sigma Cumul flags t u
-      else
-	try unify_0 env sigma Cumul flags t u
-	with e when precatchable_exception e ->
-	  unify_0 env sigma Cumul flags u t
-    with e when precatchable_exception e ->
-      (sigma,[],[])
+  let t = nf_betaiota sigma (nf_meta sigma t) in
+    unify_0 env sigma CUMUL flags t u
 
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
-  if occur_meta_or_existential mvty or is_arity env sigma mvty then
-    unify_to_type env sigma flags c status mvty
-  else (sigma,[],[])
+  let mvty = nf_meta sigma mvty in
+    unify_to_type env sigma 
+      {flags with modulo_delta = flags.modulo_delta_types;
+	 modulo_conv_on_closed_terms = Some flags.modulo_delta_types;
+	 modulo_betaiota = true}
+      c status mvty
 
 (* Move metas that may need coercion at the end of the list of instances *)
 
@@ -628,8 +836,8 @@ let order_metas metas =
 
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
-let solve_simple_evar_eqn env evd ev rhs =
-  let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
+let solve_simple_evar_eqn ts env evd ev rhs =
+  let evd,b = solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) in
   if not b then error_cannot_unify env evd (mkEvar ev,rhs);
   Evarconv.consider_remaining_unif_problems env evd
 
@@ -642,28 +850,32 @@ let w_merge env with_types flags (evd,metas,evars) =
 
     (* Process evars *)
     match evars with
-    | ((evn,_ as ev),rhs)::evars' ->
-    	if is_defined_evar evd ev then
+    | (curenv,(evk,_ as ev),rhs)::evars' ->
+	if Evd.is_defined evd evk then
 	  let v = Evd.existential_value evd ev in
 	  let (evd,metas',evars'') =
-	    unify_0 env evd topconv flags rhs v in
+	    unify_0 curenv evd CONV flags rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
+	  (* This can make rhs' ill-typed if metas are *)
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
 	  | App (f,cl) when occur_meta rhs' ->
-	      if occur_evar evn rhs' then
-                error_occur_check env evd evn rhs';
-	      if is_mimick_head f then
-		let evd' = mimick_evar evd flags f (Array.length cl) evn in
-		  w_merge_rec evd' metas evars eqns
+	      if occur_evar evk rhs' then
+                error_occur_check curenv evd evk rhs';
+	      if is_mimick_head flags.modulo_delta f then
+		let evd' =
+		  mimick_undefined_evar evd flags f (Array.length cl) evk in
+		w_merge_rec evd' metas evars eqns
 	      else
-		let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
-	  	  w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
-		    metas evars' eqns
+		let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
+		w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'')
+		  metas evars' eqns
+
           | _ ->
-	      w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
-		metas evars' eqns
+	      let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
+		w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'')
+		  metas evars' eqns
 	end
     | [] ->
 
@@ -679,7 +891,8 @@ let w_merge env with_types flags (evd,metas,evars) =
               (* No coercion needed: delay the unification of types *)
 	      ((evd,c),([],[])),(mv,status,c)::eqns
 	  else
-	    ((evd,c),([],[])),eqns in
+	    ((evd,c),([],[])),eqns 
+	in
 	  if meta_defined evd mv then
 	    let {rebus=c'},(status',_) = meta_fvalue evd mv in
             let (take_left,st,(evd,metas',evars')) =
@@ -692,23 +905,30 @@ let w_merge env with_types flags (evd,metas,evars) =
               w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns
     	  else
 	    let evd' = meta_assign mv (c,(status,TypeProcessed)) evd in
-	      w_merge_rec evd' (metas@metas'') evars'' eqns
+	      w_merge_rec evd' (metas''@metas) evars'' eqns
     | [] ->
-
-    (* Process type eqns *)
-    match eqns with
-    | (mv,status,c)::eqns ->
-        let (evd,metas,evars) = unify_type env evd flags mv status c in
-        w_merge_rec evd metas evars eqns
-    | [] -> evd
-
-  and mimick_evar evd flags hdc nargs sp =
-    let ev = Evd.find evd sp in
+	(* Process type eqns *)
+	let rec process_eqns failures = function
+	  | (mv,status,c)::eqns ->
+              (match (try Inl (unify_type env evd flags mv status c)
+		      with e -> Inr e)
+	       with 
+	       | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
+	       | Inl (evd,metas,evars) ->
+		   w_merge_rec evd metas evars (List.map fst failures @ eqns))
+	  | [] -> 
+	      (match failures with
+	       | [] -> evd
+	       | ((mv,status,c),e)::_ -> raise e)
+	in process_eqns [] eqns
+	      
+  and mimick_undefined_evar evd flags hdc nargs sp =
+    let ev = Evd.find_undefined evd sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
-      unify_0 sp_env evd' Cumul flags
-        (Retyping.get_type_of sp_env evd' c) ev.evar_concl in
+      unify_0 sp_env evd' CUMUL flags
+        (get_type_of sp_env evd' c) ev.evar_concl in
     let evd''' = w_merge_rec evd'' mc ec [] in
     if evd' == evd'''
     then Evd.define sp c evd'''
@@ -733,33 +953,47 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
 
 let check_types env flags (sigma,_,_ as subst) m n =
   if isEvar_or_Meta (fst (whd_stack sigma m)) then
-    unify_0_with_initial_metas subst true env Cumul
+    unify_0_with_initial_metas subst true env CUMUL
       flags
-      (Retyping.get_type_of env sigma n)
-      (Retyping.get_type_of env sigma m)
+      (get_type_of env sigma n)
+      (get_type_of env sigma m)
   else if isEvar_or_Meta (fst (whd_stack sigma n)) then
-    unify_0_with_initial_metas subst true env Cumul
+    unify_0_with_initial_metas subst true env CUMUL
       flags
-      (Retyping.get_type_of env sigma m)
-      (Retyping.get_type_of env sigma n)
+      (get_type_of env sigma m)
+      (get_type_of env sigma n)
   else subst
 
-let w_unify_core_0 env with_types cv_pb flags m n evd =
+let try_resolve_typeclasses env evd flags m n =
+  if flags.resolve_evars then
+    try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
+	  ~fail:true env evd
+    with e when Typeclasses_errors.unsatisfiable_exception e ->
+      error_cannot_unify env evd (m, n)
+  else evd
+
+let w_unify_core_0 env evd with_types cv_pb flags m n =
   let (mc1,evd') = retract_coercible_metas evd in
   let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in
   let subst2 =
-     unify_0_with_initial_metas (evd',ms,es) true env cv_pb flags m n
+     unify_0_with_initial_metas (evd',ms,es) false env cv_pb flags m n
   in
   let evd = w_merge env with_types flags subst2 in
-    if flags.resolve_evars then
-      try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:false
-	~fail:true env evd
-      with e when Typeclasses_errors.unsatisfiable_exception e ->
-	error_cannot_unify env evd (m, n)
-    else evd
+  try_resolve_typeclasses env evd flags m n
 
-let w_unify_0 env = w_unify_core_0 env false
-let w_typed_unify env = w_unify_core_0 env true
+let w_unify_0 env evd = w_unify_core_0 env evd false
+let w_typed_unify env evd = w_unify_core_0 env evd true
+
+let w_typed_unify_list env evd flags f1 l1 f2 l2 =
+  let flags' = { flags with resolve_evars = false } in
+  let f1,l1,f2,l2 = adjust_app_list_size f1 l1 f2 l2 in
+  let (mc1,evd') = retract_coercible_metas evd in
+  let subst =
+    List.fold_left2 (fun subst m n ->
+      unify_0_with_initial_metas subst true env CONV flags' m n) (evd',[],[])
+      (f1::l1) (f2::l2) in
+  let evd = w_merge env true flags subst in
+  try_resolve_typeclasses env evd flags (applist(f1,l1)) (applist(f2,l2))
 
 (* takes a substitution s, an open term op and a closed term cl
    try to find a subterm of cl which matches op, if op is just a Meta
@@ -777,12 +1011,12 @@ let iter_fail f a =
 (* Tries to find an instance of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] until it finds a match.
    Fails if no match is found *)
-let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
+let w_unify_to_subterm env evd ?(flags=default_unify_flags) (op,cl) =
   let rec matchrec cl =
     let cl = strip_outer_cast cl in
     (try
        if closed0 cl && not (isEvar cl)
-       then w_typed_unify env topconv flags op cl evd,cl
+       then w_typed_unify env evd CONV flags op cl,cl
        else error "Bound 1"
      with ex when precatchable_exception ex ->
        (match kind_of_term cl with
@@ -832,12 +1066,12 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
-    raise (PretypeError (env,NoOccurrenceFound (op, None)))
+    raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
 
 (* Tries to find all instances of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] and return all the matches.
    Fails if no match is found *)
-let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
+let w_unify_to_subterm_all env evd ?(flags=default_unify_flags) (op,cl) =
   let return a b =
     let (evd,c as a) = a () in
       if List.exists (fun (evd',c') -> eq_constr c c') b then b else a :: b
@@ -862,7 +1096,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
     let cl = strip_outer_cast cl in
       (bind
 	  (if closed0 cl
-	  then return (fun () -> w_typed_unify env topconv flags op cl evd,cl)
+	  then return (fun () -> w_typed_unify env evd CONV flags op cl,cl)
             else fail "Bound 1")
           (match kind_of_term cl with
 	    | App (f,args) ->
@@ -894,61 +1128,65 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
   in
   let res = matchrec cl [] in
   if res = [] then
-    raise (PretypeError (env,NoOccurrenceFound (op, None)))
+    raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))
   else
     res
 
-let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
+let w_unify_to_subterm_list env evd flags hdmeta oplist t =
   List.fold_right
     (fun op (evd,l) ->
       let op = whd_meta evd op in
       if isMeta op then
-	if allow_K then (evd,op::l)
+	if flags.allow_K_in_toplevel_higher_order_unification then (evd,op::l)
 	else error_abstraction_over_meta env evd hdmeta (destMeta op)
       else if occur_meta_or_existential op then
         let (evd',cl) =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
-	    w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
-	  with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
+	    w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
+	  with PretypeError (env,_,NoOccurrenceFound _) when
+              flags.allow_K_in_toplevel_higher_order_unification -> (evd,op)
         in
-	  if not allow_K && (* ensure we found a different instance *)
+	  if not flags.allow_K_in_toplevel_higher_order_unification &&
+            (* ensure we found a different instance *)
 	    List.exists (fun op -> eq_constr op cl) l
 	  then error_non_linear_unification env evd hdmeta cl
 	  else (evd',cl::l)
-      else if allow_K or dependent op t then
+      else if flags.allow_K_in_toplevel_higher_order_unification or dependent op t
+      then
 	(evd,op::l)
       else
 	(* This is not up to delta ... *)
-	raise (PretypeError (env,NoOccurrenceFound (op, None))))
+	raise (PretypeError (env,evd,NoOccurrenceFound (op, None))))
     oplist
     (evd,[])
 
-let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
+let secondOrderAbstraction env evd flags typ (p, oplist) =
   (* Remove delta when looking for a subterm *)
   let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
-  let (evd',cllist) =
-    w_unify_to_subterm_list env flags allow_K p oplist typ evd in
+  let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
   let pred = abstract_list_all env evd' typp typ cllist in
-  w_merge env false flags (evd',[p,pred,(ConvUpToEta 0,TypeProcessed)],[])
+  w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[])
+
+let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
+  let typp = Typing.meta_type evd p in
+  let pred = abstract_list_all_with_dependencies env evd typp typ oplist in
+  w_merge env false flags (evd,[p,pred,(Conv,TypeProcessed)],[])
+
+let secondOrderAbstractionAlgo dep =
+  if dep then secondOrderDependentAbstraction else secondOrderAbstraction
 
-let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
+let w_unify2 env evd flags dep cv_pb ty1 ty2 =
   let c1, oplist1 = whd_stack evd ty1 in
   let c2, oplist2 = whd_stack evd ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
-	let evd' =
-          secondOrderAbstraction env flags allow_K ty2 (p1,oplist1) evd in
-        (* Resume first order unification *)
-	w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd'
+        secondOrderAbstractionAlgo dep env evd flags ty2 (p1,oplist1)
     | _, Meta p2 ->
         (* Find the predicate *)
-	let evd' =
-          secondOrderAbstraction env flags allow_K ty1 (p2, oplist2) evd in
-        (* Resume first order unification *)
-	w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
+        secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2)
     | _ -> error "w_unify2"
 
 (* The unique unification algorithm works like this: If the pattern is
@@ -971,8 +1209,7 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
    Before, second-order was used if the type of Meta(1) and [x:A]t was
    convertible and first-order otherwise. But if failed if e.g. the type of
    Meta(1) had meta-variables in it. *)
-let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
-  let cv_pb = of_conv_pb cv_pb in
+let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 =
   let hd1,l1 = whd_stack evd ty1 in
   let hd2,l2 = whd_stack evd ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
@@ -980,22 +1217,27 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
 	  when List.length l1 = List.length l2 ->
 	  (try
-	      w_typed_unify env cv_pb flags ty1 ty2 evd
+	      w_typed_unify_list env evd flags hd1 l1 hd2 l2
 	    with ex when precatchable_exception ex ->
 	      try
-		w_unify2 env flags allow_K cv_pb ty1 ty2 evd
-	      with PretypeError (env,NoOccurrenceFound _) as e -> raise e)
+		w_unify2 env evd flags false cv_pb ty1 ty2
+	      with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e)
 
       (* Second order case *)
       | (Meta _, true, _, _ | _, _, Meta _, true) ->
 	  (try
-	      w_unify2 env flags allow_K cv_pb ty1 ty2 evd
-	    with PretypeError (env,NoOccurrenceFound _) as e -> raise e
+	      w_unify2 env evd flags false cv_pb ty1 ty2
+	    with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
 	      | ex when precatchable_exception ex ->
 		  try
-		    w_typed_unify env cv_pb flags ty1 ty2 evd
+		    w_typed_unify_list env evd flags hd1 l1 hd2 l2
 		  with ex' when precatchable_exception ex' ->
-		    raise ex)
+                    (* Last chance, use pattern-matching with typed
+                       dependencies (done late for compatibility) *)
+	            try
+	              w_unify2 env evd flags true cv_pb ty1 ty2
+		    with ex' when precatchable_exception ex' ->
+		      raise ex)
 
       (* General case: try first order *)
-      | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
+      | _ -> w_typed_unify env evd cv_pb flags ty1 ty2