Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

32 files changed, 355 insertions, 279 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fdb19d37..fcbe90b6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -285,11 +285,13 @@ let inductive_template evdref env tmloc ind =
    applist (mkIndU indu,List.rev evarl)
 
 let try_find_ind env sigma typ realnames =
-  let (IndType(_,realargs) as ind) = find_rectype env sigma typ in
+  let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in
   let names =
     match realnames with
       | Some names -> names
-      | None -> List.make (List.length realargs) Anonymous in
+      | None ->
+          let ind = fst (fst (dest_ind_family indf)) in
+          List.make (inductive_nrealdecls ind) Anonymous in
   IsInd (typ,ind,names)
 
 let inh_coerce_to_ind evdref env loc ty tyi =
@@ -730,7 +732,17 @@ let set_declaration_name x (_,c,t) = (x,c,t)
 
 let recover_initial_subpattern_names = List.map2 set_declaration_name
 
-let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
+let recover_and_adjust_alias_names names sign =
+  let rec aux = function
+  | [],[] ->
+      []
+  | x::names, (_,None,t)::sign ->
+      (x,(alias_of_pat x,None,t)) :: aux (names,sign)
+  | names, (na,(Some _ as c),t)::sign ->
+      (PatVar (Loc.ghost,na),(na,c,t)) :: aux (names,sign)
+  | _ -> assert false
+  in
+  List.split (aux (names,sign))
 
 let push_rels_eqn sign eqn =
   {eqn with
@@ -1644,7 +1656,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
   in
   aux (0,extenv,subst0) t0
 
-let build_tycon loc env tycon_env subst tycon extenv evdref t =
+let build_tycon loc env tycon_env s subst tycon extenv evdref t =
   let t,tt = match t with
     | None ->
 	(* This is the situation we are building a return predicate and
@@ -1659,6 +1671,8 @@ let build_tycon loc env tycon_env subst tycon extenv evdref t =
         let evd,tt = Typing.e_type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
+  let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
+  if not b then anomaly (Pp.str "Build_tycon: should be a type");
   { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -1693,11 +1707,12 @@ let build_inversion_problem loc env sigma tms t =
 	let pat,acc = make_patvar t acc in
 	let indf' = lift_inductive_family n indf in
 	let sign = make_arity_signature env true indf' in
-	let sign = recover_alias_names alias_of_pat (pat :: List.rev patl) sign in
-	let p = List.length realargs in
+        let patl = pat :: List.rev patl in
+	let patl,sign = recover_and_adjust_alias_names patl sign in
+	let p = List.length patl in
 	let env' = push_rel_context sign env in
-	let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
-	patl@pat::patl',acc_sign,acc
+	let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
+	List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
       let d = (alias_of_pat pat,None,typ) in
@@ -1780,7 +1795,7 @@ let build_inversion_problem loc env sigma tms t =
       mat       = [eqn1;eqn2];
       caseloc   = loc;
       casestyle = RegularStyle;
-      typing_function = build_tycon loc env pb_env subst} in
+      typing_function = build_tycon loc env pb_env s subst} in
   let pred = (compile pb).uj_val in
   (!evdref,pred)
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 559f5fe6..055996de 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -60,9 +60,9 @@ let coe_info_typ_equal c1 c2 =
 
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
-  | CL_CONST c1, CL_CONST c2 -> con_user_ord c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> con_user_ord c1 c2
-  | CL_IND i1, CL_IND i2 -> ind_user_ord i1 i2
+  | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2
+  | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
 module ClTyp = struct
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a6e2bc19..161cffa8 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -351,34 +351,45 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx next =
     else mkresult subst (mk_ctx (mkMeta special_meta)) next
   with PatternMatchingFailure -> next ()
 
+let subargs env v = Array.map_to_list (fun c -> (env, c)) v
+
 (* Tries to match a subterm of [c] with [pat] *)
 let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
   let rec aux env c mk_ctx next =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
-      let next () = try_aux [env] [c1] next_mk_ctx next in
+      let next_mk_ctx = function
+      | [c1] -> mk_ctx (mkCast (c1, k, c2))
+      | _ -> assert false
+      in
+      let next () = try_aux [env, c1] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Lambda (x,c1,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
+      let next_mk_ctx = function
+      | [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
+      | _ -> assert false
+      in
       let next () = 
 	let env' = Environ.push_rel (x,None,c1) env in
-	  try_aux [env;env'] [c1; c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Prod (x,c1,c2) ->
-      let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
+      let next_mk_ctx = function
+      | [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
+      | _ -> assert false
+      in
       let next () = 
 	let env' = Environ.push_rel (x,None,c1) env in
-	  try_aux [env;env'] [c1;c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
-      | [c1;c2] -> mkLetIn (x,c1,t,c2)
+      | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
       | _ -> assert false
       in
       let next () = 
 	let env' = Environ.push_rel (x,Some c1,t) env in
-	  try_aux [env;env'] [c1;c2] next_mk_ctx next in
+        try_aux [(env, c1); (env', c2)] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | App (c1,lc) ->
       let next () =
@@ -390,14 +401,15 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             let mk_ctx = function
               | [app';c] -> mk_ctx (mkApp (app',[|c|]))
               | _ -> assert false in
-            try_aux [env] [app;Array.last lc] mk_ctx next
+            try_aux [(env, app); (env, Array.last lc)] mk_ctx next
           else
             let rec aux2 app args next =
               match args with
               | [] ->
                   let mk_ctx le =
                     mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-                  try_aux [env] (c1::Array.to_list lc) mk_ctx next
+                  let sub = (env, c1) :: subargs env lc in
+                  try_aux sub mk_ctx next
               | arg :: args ->
                   let app = mkApp (app,[|arg|]) in
                   let next () = aux2 app args next in
@@ -407,7 +419,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
         else
           let mk_ctx le =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
-          try_aux [env] (c1::Array.to_list lc) mk_ctx next
+          let sub = (env, c1) :: subargs env lc in
+          try_aux sub mk_ctx next
       in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Case (ci,hd,c1,lc) ->
@@ -415,24 +428,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in
+      let sub = (env, c1) :: subargs env lc in
+      let next () = try_aux sub next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next () =
-      try_aux
-	[env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+    let sub = subargs env types @ subargs env bodies in
+    let next () = try_aux sub next_mk_ctx next in
     authorized_occ env sigma partial_app closed pat c mk_ctx next
   | CoFix (i,(names,types,bodies)) ->
     let nb_fix = Array.length types in
     let next_mk_ctx le =
       let (ntypes,nbodies) = CList.chop nb_fix le in
       mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
-    let next () =
-      try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in
+    let sub = subargs env types @ subargs env bodies in
+    let next () = try_aux sub next_mk_ctx next in
     authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Proj (p,c') ->
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
@@ -441,27 +454,24 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
 	try 
 	  let term = Retyping.expand_projection env sigma p c' [] in
 	    aux env term mk_ctx next
-	with Retyping.RetypeError _ -> raise PatternMatchingFailure
+	with Retyping.RetypeError _ -> next ()
       else
-	try_aux [env] [c'] next_mk_ctx next in
+      try_aux [env, c'] next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
       authorized_occ env sigma partial_app closed pat c mk_ctx next
 
   (* Tries [sub_match] for all terms in the list *)
-  and try_aux lenv lc mk_ctx next =
-    let rec try_sub_match_rec lacc lenv lc = 
-      match lenv, lc with
-      | _, [] -> next ()
-      | env :: tlenv, c::tl ->
-          let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in
-          let next () = 
-	    let env' = match tlenv with [] -> lenv | _ -> tlenv in
-	      try_sub_match_rec (c::lacc) env' tl 
-	  in
-            aux env c mk_ctx next 
-      | _ -> assert false in
-    try_sub_match_rec [] lenv lc in
+  and try_aux lc mk_ctx next =
+    let rec try_sub_match_rec lacc lc =
+      match lc with
+      | [] -> next ()
+      | (env, c) :: tl ->
+        let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in
+        let next () = try_sub_match_rec (c :: lacc) tl in
+        aux env c mk_ctx next
+    in
+    try_sub_match_rec [] lc in
   let lempty () = IStream.Nil in
   let result () = aux env c (fun x -> x) lempty in
   IStream.thunk result
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 046ee0da..28fb8cbe 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -498,16 +498,17 @@ let rec detype flags avoid env sigma t =
 	  else noparams ()
 
     | Evar (evk,cl) ->
-        let bound_to_itself id c =
+        let bound_to_itself_or_letin (id,b,_) c =
+          b != None ||
 	  try let n = List.index Name.equal (Name id) (fst env) in 
-	      isRelN n c 
+	      isRelN n c
 	  with Not_found -> isVarId id c in
       let id,l =
         try
           let id = Evd.evar_ident evk sigma in
-          let l = Evd.evar_instance_array bound_to_itself (Evd.find sigma evk) cl in
-          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> (Id.Set.union fvs (collect_vars c), Int.Set.union rels (free_rels c))) (Id.Set.empty,Int.Set.empty) l in
-          let l = Evd.evar_instance_array (fun id c -> not !print_evar_arguments && (bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
+          let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
+          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
+          let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a95af253..f388f900 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
-      let evd, b = 
-	try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 
-	with Univ.UniverseInconsistency _ -> evd, false
+      let evd, e = 
+	try
+	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
+	    env evd term1 term2 
+	  in
+	    if b then evd, None
+	    else evd, Some (ConversionFailed (env,term1,term2))
+	with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e)
       in
-	if b then Some (evd, true)
-	else if is_ground_env evd env then Some (evd, false)
-	else None)
+	match e with
+	| None -> Some (evd, e)
+	| Some e -> 
+	  if is_ground_env evd env then Some (evd, Some e)
+	  else None)
     else None
   in
   match ground_test with
-    | Some (evd, true) -> Success evd
-    | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2))
+    | Some (evd, None) -> Success evd
+    | Some (evd, Some e) -> UnifFailure (evd,e)
     | None ->
 	(* Until pattern-unification is used consistently, use nohdbeta to not
 	   destroy beta-redexes that can be used for 1st-order unification *)
@@ -555,8 +562,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
         let f1 i =
           ise_and i
-	    [(fun i -> evar_conv_x ts env i CONV t1 t2);
-	     (fun i -> evar_conv_x ts env i CONV b1 b2);
+	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 5aa72c90..bfd19c6c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -64,30 +64,33 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     in
       modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
-    mkProd (na,u,refresh dir v)
+      mkProd (na,u,refresh dir v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
-  and refresh_term_evars onevars t =
+  and refresh_term_evars onevars top t =
     match kind_of_term t with
     | App (f, args) when is_template_polymorphic env f ->
       let pos = get_polymorphic_positions f in
 	refresh_polymorphic_positions args pos
+    | App (f, args) when top && isEvar f -> 
+      refresh_term_evars true false f; 
+      Array.iter (refresh_term_evars onevars false) args
     | Evar (ev, a) when onevars ->
       let evi = Evd.find !evdref ev in
       let ty' = refresh true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
-    | _ -> iter_constr (refresh_term_evars onevars) t
+    | _ -> iter_constr (refresh_term_evars onevars false) t
   and refresh_polymorphic_positions args pos =
     let rec aux i = function
       | Some l :: ls -> 
         if i < Array.length args then 
-	  ignore(refresh_term_evars true args.(i));
+	  ignore(refresh_term_evars true false args.(i));
         aux (succ i) ls
       | None :: ls -> 
         if i < Array.length args then 
-          ignore(refresh_term_evars false args.(i));
+          ignore(refresh_term_evars false false args.(i));
 	aux (succ i) ls
       | [] -> ()
     in aux 0 pos
@@ -97,7 +100,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
       (match pbty with
       | None -> t
       | Some dir -> refresh dir t)
-    else (refresh_term_evars false t; t)
+    else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
 
@@ -118,11 +121,11 @@ let is_success = function Success _ -> true | UnifFailure _ -> false
 let test_success conv_algo env evd c c' rhs =
   is_success (conv_algo env evd c c' rhs)
 
-let add_conv_oriented_pb (pbty,env,t1,t2) evd =
+let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
   match pbty with
-  | Some true -> add_conv_pb (Reduction.CUMUL,env,t1,t2) evd
-  | Some false -> add_conv_pb (Reduction.CUMUL,env,t2,t1) evd
-  | None -> add_conv_pb (Reduction.CONV,env,t1,t2) evd
+  | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
+  | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
+  | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd
 
 (*------------------------------------*
  * Restricting existing evars         *
@@ -175,20 +178,31 @@ let restrict_instance evd evk filter argsv =
   Filter.filter_array (Filter.compose (evar_filter evi) filter) argsv
 
 let noccur_evar env evd evk c =
-  let rec occur_rec k c = match kind_of_term c with
+  let cache = ref Int.Set.empty (* cache for let-ins *) in
+  let rec occur_rec (k, env as acc) c =
+  match kind_of_term c with
   | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
-       | Some c -> occur_rec k c
+       | Some c -> occur_rec acc c
        | None ->
            if Evar.equal evk evk' then raise Occur
-           else Array.iter (occur_rec k) args')
+           else Array.iter (occur_rec acc) args')
   | Rel i when i > k ->
-      (match pi2 (Environ.lookup_rel (i-k) env) with
+      if not (Int.Set.mem (i-k) !cache) then
+      (match pi2 (Environ.lookup_rel i env) with
        | None -> ()
-       | Some b -> occur_rec k (lift i b))
-  | _ -> iter_constr_with_binders succ occur_rec k c
+       | Some b -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b))
+  | Proj (p,c) -> 
+    let c = 
+      try Retyping.expand_projection env evd p c []
+      with Retyping.RetypeError _ -> 
+	(* Can happen when called from w_unify which doesn't assign evars/metas 
+	   eagerly enough *) c
+    in occur_rec acc c
+  | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env))
+    occur_rec acc c
   in
-  try occur_rec 0 c; true with Occur -> false
+  try occur_rec (0,env) c; true with Occur -> false
 
 (***************************************)
 (* Managing chains of local definitons *)
@@ -213,7 +227,7 @@ let compute_var_aliases sign =
     sign Id.Map.empty
 
 let compute_rel_aliases var_aliases rels =
-  snd (List.fold_right (fun (_,b,t) (n,aliases) ->
+  snd (List.fold_right (fun (_,b,u) (n,aliases) ->
     (n-1,
      match b with
      | Some t ->
@@ -227,7 +241,7 @@ let compute_rel_aliases var_aliases rels =
                try Int.Map.find (p+n) aliases with Not_found -> [] in
              Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
          | _ ->
-             Int.Map.add n [lift n t] aliases)
+             Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
      | None -> aliases))
          rels (List.length rels,Int.Map.empty))
 
@@ -311,6 +325,7 @@ let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
   let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
+  let acc3 = ref Int.Set.empty and acc4 = ref Id.Set.empty in
   let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
   let is_in_cache depth = function
     | Rel n -> Int.Set.mem (n-depth) !cache_rel
@@ -325,8 +340,13 @@ let free_vars_and_rels_up_alias_expansion aliases c =
     | Rel _ | Var _ as ck ->
       if is_in_cache depth ck then () else begin
       put_in_cache depth ck;
-      let c = expansion_of_var aliases c in
+      let c' = expansion_of_var aliases c in
+      (if c != c' then (* expansion, hence a let-in *)
         match kind_of_term c with
+        | Var id -> acc4 := Id.Set.add id !acc4
+        | Rel n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3
+        | _ -> ());
+      match kind_of_term c' with
         | Var id -> acc2 := Id.Set.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
@@ -338,7 +358,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
           frec (aliases,depth) c
   in
   frec (aliases,0) c;
-  (!acc1,!acc2)
+  (!acc1,!acc2,!acc3,!acc4)
 
 (********************************)
 (* Managing pattern-unification *)
@@ -374,7 +394,7 @@ let get_actual_deps aliases l t =
     l
   else
     (* Probably strong restrictions coming from t being evar-closed *)
-    let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+    let (fv_rels,fv_ids,_,_) = free_vars_and_rels_up_alias_expansion aliases t in
     List.filter (fun c ->
       match kind_of_term c with
       | Var id -> Id.Set.mem id fv_ids
@@ -1013,52 +1033,52 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t =
-  let f,args = decompose_app_vect t in
+let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
+  let f,args2 = decompose_app_vect t in
+  let f,args1 = decompose_app_vect (whd_evar evd f) in
+  let args = Array.append args1 args2 in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
     let n = Inductiveops.inductive_nparams ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false k g t1 && is_constrainable_in false k g t2
+      Array.for_all (is_constrainable_in false evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
+  | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
   | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) true
 
-let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
-  let t = expansion_of_var aliases t in
-  match kind_of_term t with
-  | Var id -> Id.Set.mem id fv_ids
-  | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true k (ev,fvs) t
-
-let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
-  let filter1 =
-    restrict_upon_filter evd evk1 (noccur_evar env evd evk2) argsv1
-  in
-  let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
-  let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
-  let filter2 =
-    restrict_upon_filter evd evk2 (noccur_evar env evd evk1) argsv2
-  in
-  let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
-  let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
-  evd,ev1,ev2
+let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t =
+  let t' = expansion_of_var aliases t in
+  if t' != t then
+    (* t is a local definition, we keep it only if appears in the list *)
+    (* of let-in variables effectively occurring on the right-hand side, *)
+    (* which is the only reason to keep it when inverting arguments *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id let_ids
+    | Rel n -> Int.Set.mem n let_rels
+    | _ -> assert false
+  else
+    (* t is an instance for a proper variable; we filter it along *)
+    (* the free variables allowed to occur *)
+    match kind_of_term t with
+    | Var id -> Id.Set.mem id fv_ids
+    | Rel n -> n <= k || Int.Set.mem n fv_rels
+    | _ -> (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
 (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
    the common domain of definition *)
-let project_evar_on_evar g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
-    (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
+    (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2)
     argsv1 in
   let candidates1 =
     try restrict_candidates g env evd filter1 ev1 ev2
@@ -1094,9 +1114,9 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
-let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) =
+let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
-    let evd,body = project_evar_on_evar g env evd aliases 0 pbty ev1 ev2 in
+    let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
     let evd' = Evd.define evk2 body evd in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
@@ -1113,27 +1133,23 @@ let preferred_orientation evd evk1 evk2 =
   | _,Evar_kinds.QuestionMark _ -> false
   | _ -> true
 
-let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env in
   if preferred_orientation evd evk1 evk2 then
-    try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+    try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
-    try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
-    try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
-    try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+    try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
-    add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
-
-let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
-  let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty =
-    (* If an evar occurs in the instance of the other evar and the
-       use of an heuristic is forced, we restrict *)
-    if force then ensure_evar_independent g env evd ev1 ev2, None
-    else (evd,ev1,ev2),pbty in
+    add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
+
+let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+  let pbty = if force then None else pbty in
   let evi = Evd.find evd evk1 in
   let evd =
     try 
@@ -1162,7 +1178,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
           downcast evk2 t2 (downcast evk1 t1 evd)
     with Reduction.NotArity -> 
       evd in
-  solve_evar_evar_aux f g env evd pbty ev1 ev2
+  solve_evar_evar_aux force f g env evd pbty ev1 ev2
 
 type conv_fun =
   env ->  evar_map -> conv_pb -> constr -> constr -> unification_result
@@ -1321,7 +1337,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         let aliases = lift_aliases k aliases in
         (try
           let ev = (evk,Array.map (lift k) argsv) in
-          let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k None ev' ev in
+          let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
           evdref := evd;
           body
         with
@@ -1338,7 +1354,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           let evd =
              (* Try to project (a restriction of) the left evar ... *)
             try
-              let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 None ev'' ev' in
+              let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
               let evd = Evd.define evk' body evd in
 		check_evar_instance evd evk' body conv_algo
             with
@@ -1384,19 +1400,6 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
             map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
               imitate envk t in
 
-  let _fast rhs = 
-    let filter_ctxt = evar_filtered_context evi in
-    let names = ref Idset.empty in
-    let rec is_id_subst ctxt s =
-       match ctxt, s with
-         | ((id, _, _) :: ctxt'), (c :: s') ->
-           names := Idset.add id !names;
-           isVarId id c && is_id_subst ctxt' s'
-         | [], [] -> true
-         | _ -> false in
-    is_id_subst filter_ctxt (Array.to_list argsv) &&
-    closed0 rhs &&
-    Idset.subset (collect_vars rhs) !names in
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d286b98e..201a16eb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,9 +212,11 @@ let whd_head_evar sigma c =
 (* Creating new metas *)
 (**********************)
 
+let meta_counter_summary_name = "meta counter"
+
 (* Generator of metavariables *)
 let new_meta =
-  let meta_ctr = Summary.ref 0 ~name:"meta counter" in
+  let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
   fun () -> incr meta_ctr; !meta_ctr
 
 let mk_new_meta () = mkMeta(new_meta())
@@ -241,9 +243,11 @@ let make_pure_subst evi args =
 (* Creating new evars *)
 (**********************)
 
+let evar_counter_summary_name = "evar counter"
+
 (* Generator of existential names *)
 let new_untyped_evar =
-  let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
   fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
 (*------------------------------------*
@@ -838,3 +842,8 @@ let subterm_source evk (loc,k) =
     | Evar_kinds.SubEvar (evk) -> evk
     | _ -> evk in
   (loc,Evar_kinds.SubEvar evk)
+
+
+(** Term exploration up to isntantiation. *)
+let kind_of_term_upto sigma t =
+  Constr.kind (Reductionops.whd_evar sigma t)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f89266a6..49036798 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
 exception Uninstantiated_evar of existential_key
 val flush_and_check_evars :  evar_map -> constr -> constr
 
+(** {6 Term manipulation up to instantiation} *)
+
+(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
+    as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
+    value of [e] in [sigma] is (recursively) used. *)
+val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
@@ -236,3 +243,6 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 
 val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
+
+val meta_counter_summary_name : string
+val evar_counter_summary_name : string
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ee72d314..bf519fb7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -230,20 +230,20 @@ let evar_instance_array test_id info args =
     else instance_mismatch ()
   | false :: filter, _ :: ctxt ->
     instrec filter ctxt i
-  | true :: filter, (id, _, _) :: ctxt ->
+  | true :: filter, (id,_,_ as d) :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
-      if test_id id c then instrec filter ctxt (succ i)
+      if test_id d c then instrec filter ctxt (succ i)
       else (id, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-    let map i (id, _, _) =
+    let map i (id,_,_ as d) =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id id c then None else Some (id,c)
+        if test_id d c then None else Some (id,c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -251,7 +251,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array isVarId info args
+  evar_instance_array (fun (id,_,_) -> isVarId id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -568,14 +568,6 @@ type evar_map = {
 
 (*** Lifting primitive from Evar.Map. ***)
 
-(* HH: The progress tactical now uses this function. *)
-let progress_evar_map d1 d2 =
-  let is_new k v =
-    assert (v.evar_body == Evar_empty);
-    EvMap.mem k d2.defn_evars
-  in
-  not (d1 == d2) && EvMap.exists is_new d1.undf_evars
-
 let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
   let id = match naming with
   | Misctypes.IntroAnonymous ->
@@ -779,7 +771,9 @@ let merge_universe_context evd uctx' =
 let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
-let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
+let add_conv_pb ?(tail=false) pb d =
+  if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
+  else {d with conv_pbs = pb::d.conv_pbs}
 
 let evar_source evk d = (find d evk).evar_source
 
@@ -1195,6 +1189,18 @@ let abstract_undefined_variables uctx =
   in { uctx with uctx_local = Univ.ContextSet.empty;
       uctx_univ_algebraic = vars' }
 
+let fix_undefined_variables ({ universes = uctx } as evm) =
+  let algs', vars' = 
+    Univ.LMap.fold (fun u v (algs, vars as acc) ->
+      if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
+      else acc)
+      uctx.uctx_univ_variables 
+      (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
+  in
+    {evm with universes = 
+	{ uctx with uctx_univ_variables = vars';
+	  uctx_univ_algebraic = algs' } }
+
 
 let refresh_undefined_univ_variables uctx =
   let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
@@ -1301,27 +1307,6 @@ let e_eq_constr_univs evdref t u =
 let eq_constr_univs_test evd t u =
   snd (eq_constr_univs evd t u)
 
-let eq_named_context_val d ctx1 ctx2 = 
-  ctx1 == ctx2 ||
-    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
-    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 
-      && (eq_constr_univs_test d) t1 t2
-    in List.equal eq_named_declaration c1 c2
-
-let eq_evar_body d b1 b2 = match b1, b2 with
-| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2
-| _ -> false
-
-let eq_evar_info d ei1 ei2 =
-  ei1 == ei2 ||
-    eq_constr_univs_test d ei1.evar_concl ei2.evar_concl &&
-    eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
-    eq_evar_body d ei1.evar_body ei2.evar_body
-    (** ppedrot: [eq_constr] may be a bit too permissive here *)
-
-
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 53f8b0db..fe785a83 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -12,7 +12,6 @@ open Names
 open Term
 open Context
 open Environ
-open Mod_subst
 
 (** {5 Existential variables and unification states}
 
@@ -127,10 +126,6 @@ type evar_map
 (** Type of unification state. Essentially a bunch of state-passing data needed
     to handle incremental term construction. *)
 
-val progress_evar_map : evar_map -> evar_map -> bool
-(** Assuming that the second map extends the first one, this says if
-   some existing evar has been refined *)
-
 val empty : evar_map
 (** The empty evar map. *)
 
@@ -205,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map
 val undefined_map : evar_map -> evar_info Evar.Map.t
 (** Access the undefined evar mapping directly. *)
 
-val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
-(** Compare the evar_info's up to the universe constraints of the evar map. *)
-
 val drop_all_defined : evar_map -> evar_map
 
 (** {6 Instantiating partial terms} *)
@@ -224,7 +216,7 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
@@ -398,7 +390,7 @@ type clbinding =
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
-val add_conv_pb :  evar_constraint -> evar_map -> evar_map
+val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->
@@ -538,6 +530,8 @@ val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> e
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
 val abstract_undefined_variables : evar_universe_context -> evar_universe_context
 
+val fix_undefined_variables : evar_map -> evar_map
+
 val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
 
 val nf_constraints : evar_map -> evar_map
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 7f7f4d76..95a6ba79 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -11,7 +11,6 @@ open Util
 open Errors
 open Names
 open Locus
-open Context
 open Term
 open Nameops
 open Termops
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 82330b84..47d9654e 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Locus
 open Context
 open Term
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 67f3cb41..e514fd52 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,9 @@ open Glob_term
 
 val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
 
+val cast_type_eq : ('a -> 'a -> bool) ->
+  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+
 val glob_constr_eq : glob_constr -> glob_constr -> bool
 
 (** Operations on [glob_constr] *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 654f914b..dfdc24d4 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -18,7 +18,6 @@ open Declarations
 open Declareops
 open Environ
 open Reductionops
-open Inductive
 
 (* The following three functions are similar to the ones defined in
    Inductive, but they expect an env *)
@@ -274,7 +273,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let ind_tags =
-    rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+    rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
   let cstr_tags =
     Array.map2 (fun c n ->
       let d,_ = decompose_prod_assum c in
@@ -366,14 +365,16 @@ let get_arity env ((ind,u),params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let parsign =
     (* Dynamically detect if called with an instance of recursively
-       uniform parameter only or also of non recursively uniform
+       uniform parameter only or also of recursively non-uniform
        parameters *)
-    let parsign = mib.mind_params_ctxt in
-    let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
-    if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then
-      snd (List.chop nnonrecparams mib.mind_params_ctxt)
-    else
-      parsign in
+    let nparams = List.length params in
+    if Int.equal nparams mib.mind_nparams then
+      mib.mind_params_ctxt
+    else begin
+      assert (Int.equal nparams mib.mind_nparams_rec);
+      let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in
+      snd (List.chop nnonrecparamdecls mib.mind_params_ctxt)
+    end in
   let parsign = Vars.subst_instance_context u parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
   let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
@@ -527,7 +528,7 @@ let type_case_branches_with_names env indspec p c =
   let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
   (* Build case type *)
-  let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
+  let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env p (ind,params) then
     (set_pattern_names env (fst ind) lbrty, conclty)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index af1783b7..7959759a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -25,7 +25,9 @@ val type_of_constructors : env -> pinductive -> types array
 (** Return constructor types in normal form *)
 val arities_of_constructors : env -> pinductive -> types array
 
-(** An inductive type with its parameters *)
+(** An inductive type with its parameters (transparently supports
+    reasoning either with only recursively uniform parameters or with all
+    parameters including the recursively non-uniform ones *)
 type inductive_family
 val make_ind_family : inductive puniverses * constr list -> inductive_family
 val dest_ind_family : inductive_family -> inductive puniverses * constr list
@@ -138,10 +140,14 @@ val lift_constructor : int -> constructor_summary -> constructor_summary
 val get_constructor :
   pinductive * mutual_inductive_body * one_inductive_body * constr list ->
   int -> constructor_summary
-val get_arity        : env -> inductive_family -> rel_context * sorts_family
 val get_constructors : env -> inductive_family -> constructor_summary array
 val get_projections  : env -> inductive_family -> constant array option
 
+(** [get_arity] returns the arity of the inductive family instantiated
+    with the parameters; if recursively non-uniform parameters are not
+    part of the inductive family, they appears in the arity *)
+val get_arity        : env -> inductive_family -> rel_context * sorts_family
+
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
 val make_arity_signature : env -> bool -> inductive_family -> rel_context
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c49bec9a..705e594a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -123,6 +123,8 @@ let head_of_constr_reference c = match kind_of_term c with
 
 let pattern_of_constr env sigma t =
   let ctx = ref [] in
+  let keep = ref Evar.Set.empty in
+  let remove = ref Evar.Set.empty in
   let rec pattern_of_constr env t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -141,28 +143,38 @@ let pattern_of_constr env sigma t =
     | App (f,a) ->
         (match
           match kind_of_term f with
-            Evar (evk,args as ev) ->
-              (match snd (Evd.evar_source evk sigma) with
-                  Evar_kinds.MatchingVar (true,id) ->
-                    ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-                    Some id
-                | _ -> None)
-            | _ -> None
-          with
-            | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
-            | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
+          | Evar (evk,args as ev) ->
+            (match snd (Evd.evar_source evk sigma) with
+              Evar_kinds.MatchingVar (true,id) ->
+		let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+                  ctx := (id,None,ty)::!ctx;
+		  keep := Evar.Set.union (evars_of_term ty) !keep;
+		  remove := Evar.Set.add evk !remove;
+                  Some id
+            | _ -> None)
+          | _ -> None
+         with
+         | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a))
+         | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a))
     | Const (sp,u)  -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
       pattern_of_constr env (Retyping.expand_projection env sigma p c [])
     | Evar (evk,ctxt as ev) ->
-        (match snd (Evd.evar_source evk sigma) with
-          | Evar_kinds.MatchingVar (b,id) ->
-              ctx := (id,None,Evarutil.nf_evar sigma (existential_type sigma ev))::!ctx;
-              assert (not b); PMeta (Some id)
-          | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt)
-          | _ -> PMeta None)
+      remove := Evar.Set.add evk !remove;
+      (match snd (Evd.evar_source evk sigma) with
+      | Evar_kinds.MatchingVar (b,id) ->
+	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+          ctx := (id,None,ty)::!ctx;
+	  let () = ignore (pattern_of_constr env ty) in
+          assert (not b); PMeta (Some id)
+      | Evar_kinds.GoalEvar -> 
+	PEvar (evk,Array.map (pattern_of_constr env) ctxt)
+      | _ -> 
+	let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in
+	let () = ignore (pattern_of_constr env ty) in
+	 PMeta None)
     | Case (ci,p,a,br) ->
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
@@ -178,9 +190,11 @@ let pattern_of_constr env sigma t =
     | Fix f -> PFix f
     | CoFix f -> PCoFix f in
   let p = pattern_of_constr env t in
+  let remove = Evar.Set.diff !remove !keep in
+  let sigma = Evar.Set.fold (fun ev acc -> Evd.remove acc ev) remove sigma in
   (* side-effect *)
   (* Warning: the order of dependencies in ctx is not ensured *)
-  (!ctx,p)
+  (sigma,!ctx,p)
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -220,7 +234,7 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
-	  snd (pattern_of_constr env sigma c)
+	  pi3 (pattern_of_constr env sigma c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
@@ -245,7 +259,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 snd (pattern_of_constr (Global.env()) Evd.empty t)
+	 pi3 (pattern_of_constr (Global.env()) Evd.empty t)
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index cf02421c..9e72280f 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,8 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> 
+  Evd.evar_map * named_context * constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 040792ef..0cadffa4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs =
        iraise (e, info));
     indexes
   else
-    (* we now search recursively amoungst all combinations *)
+    (* we now search recursively among all combinations *)
     (try
        List.iter
 	 (fun l ->
@@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
-(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
 (* Utilisé pour inférer le prédicat des Cases *)
@@ -324,12 +324,6 @@ let pretype_id pretype loc env evdref lvar id =
       (* Check if [id] is a section or goal variable *)
       try
 	let (_,_,typ) = lookup_named id env in
-	(* let _ =  *)
-	(*   try  *)
-   	(*     let ctx = Decls.variable_context id in *)
-	(*       evdref := Evd.merge_context_set univ_rigid !evdref ctx; *)
-	(*   with Not_found -> () *)
-	(* in *)
 	  { uj_val  = mkVar id; uj_type = typ }
       with Not_found ->
 	  (* [id] not found, standard error message *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7d1e0c9b..142b5451 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags
 
 val all_and_fail_flags : inference_flags
 
-(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
 (** Generic call to the interpreter from glob_constr to open_constr, leaving
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a23963ab..dd671f11 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -60,13 +60,20 @@ module ReductionBehaviour = struct
 
   let discharge = function
     | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
-       let c' = pop_con c in
-       let vars, _subst, _ctx = Lib.section_segment_of_constant c in
-       let extra = List.length vars in
-       let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
-       let recargs' = List.map ((+) extra) b.b_recargs in
-       let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in
-       Some (ReqGlobal (ConstRef c', req), (ConstRef c', b'))
+      let b =
+        if Lib.is_in_section (ConstRef c) then
+          let vars, _, _ = Lib.section_segment_of_constant c in
+          let extra = List.length vars in
+          let nargs' =
+             if b.b_nargs = max_int then max_int
+             else if b.b_nargs < 0 then b.b_nargs
+             else b.b_nargs + extra in
+          let recargs' = List.map ((+) extra) b.b_recargs in
+          { b with b_nargs = nargs'; b_recargs = recargs' }
+        else b
+      in
+      let c = Lib.discharge_con c in
+      Some (ReqGlobal (ConstRef c, req), (ConstRef c, b))
     | _ -> None
 
   let rebuild = function
@@ -842,7 +849,14 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		    let (tm',sk'),cst_l' =
 		      whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
 		    in
-		      if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk'
+		    let rec is_case x = match kind_of_term x with
+		      | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+		      | App (hd, _) -> is_case hd
+		      | Case _ -> true
+		      | _ -> false in
+		    if equal_stacks (x, app_sk) (tm', sk')
+		       || Stack.will_expose_iota sk'
+		       || is_case tm'
 		      then fold ()
 		      else whrec cst_l' (tm', sk' @ sk)
 		  else match recargs with
@@ -980,7 +994,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
 	  reduce_and_refold_cofix whrec env cst_l cofix stack
 	|_ -> fold ()
       else fold ()
@@ -1059,7 +1073,7 @@ let local_whd_state_gen flags sigma =
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
-	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
 	  whrec (contract_cofix cofix, stack)
 	|_ -> s
       else s
@@ -1279,7 +1293,8 @@ let sigma_univ_state =
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
+let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
+    env sigma x y = 
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1301,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
-  | Univ.UniverseInconsistency _ -> sigma, false
+  | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
@@ -1617,3 +1632,16 @@ let head_unfold_under_prod ts env _ c =
 	    | Const cst -> beta_applist (unfold cst,l)
 	    | _ -> c in
   aux c
+
+let betazetaevar_applist sigma n c l =
+  let rec stacklam n env t stack =
+    if Int.equal n 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+    | Evar ev, _ ->
+      (match safe_evar_value sigma ev with
+      | Some body -> stacklam n env body stack
+      | None -> applist (substl env t, stack))
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 7c61d4e1..1df2a73b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -268,9 +268,11 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 
 (** [infer_fconv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
+    @raises UniverseInconsistency iff catch_incon is set to false, 
+    otherwise returns false in that case.
  *)
-val infer_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> 
-  evar_map * bool
+val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
+  env -> evar_map -> constr -> constr -> evar_map * bool
 
 (** {6 Special-Purpose Reduction Functions } *)
 
@@ -278,6 +280,7 @@ val whd_meta : evar_map -> constr -> constr
 val plain_instance : constr Metamap.t -> constr -> constr
 val instance : evar_map -> constr Metamap.t -> constr -> constr
 val head_unfold_under_prod : transparent_state -> reduction_function
+val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
 
 (** {6 Heuristic for Conversion with Evar } *)
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index cd52ba44..a56861c6 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -100,7 +100,7 @@ let retype ?(polyprop=true) sigma =
     | Ind ind -> rename_type_of_inductive env ind
     | Construct cstr -> rename_type_of_constructor env cstr
     | Case (_,p,c,lf) ->
-        let Inductiveops.IndType(_,realargs) =
+        let Inductiveops.IndType(indf,realargs) =
           let t = type_of env c in
           try Inductiveops.find_rectype env sigma t
           with Not_found ->
@@ -109,7 +109,8 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let t = whd_beta sigma (applist (p, realargs)) in
+        let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
+        let t = betazetaevar_applist sigma n p realargs in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b4e0459c..372b26aa 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,7 +23,6 @@ open Reductionops
 open Cbv
 open Patternops
 open Locus
-open Pretype_errors
 
 (* Errors *)
 
@@ -190,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
              if
 	       Array.for_all (noccurn k) tys
 	       && Array.for_all (noccurn (k+nbfix)) bds
+	       && k <= n
 	     then
 	       (k, List.nth labs (k-1))
 	     else
@@ -597,13 +597,6 @@ let reduce_proj env sigma whfun whfun' c =
     | _ -> raise Redelimination
   in redrec c
 
-
-let dont_expose_case = function
-  | EvalVar _ | EvalRel _ | EvalEvar _ -> false
-  | EvalConst c ->
-     Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z)
-		 false (ReductionBehaviour.get (ConstRef c))
-
 let whd_nothing_for_iota env sigma s =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
@@ -1212,9 +1205,10 @@ let one_step_reduce env sigma c =
 	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_construct_stack env) sigma fix stack with
+	  (try match reduce_fix (whd_construct_stack env) sigma fix stack with
              | Reduced s' -> s'
-	     | NotReducible -> raise NotStepReducible)
+	     | NotReducible -> raise NotStepReducible
+           with Redelimination -> raise NotStepReducible)
       | _ when isEvalRef env x ->
 	  let ref,u = destEvalRefU x in
           (try
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5862a852..9f04faa8 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -15,7 +15,6 @@ open Term
 open Vars
 open Context
 open Environ
-open Locus
 
 (* Sorts and sort family *)
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9f3efd72..2552c67e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -11,7 +11,6 @@ open Names
 open Term
 open Context
 open Environ
-open Locus
 
 (** printers *)
 val print_sort : sorts -> std_ppcmds
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 817d6878..18e83056 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -14,7 +14,6 @@ open Term
 open Vars
 open Context
 open Evd
-open Environ
 open Util
 open Typeclasses_errors
 open Libobject
@@ -427,7 +426,6 @@ let add_class cl =
   cl.cl_projs
 
 
-open Declarations
       
 (*
  * interface functions
@@ -485,15 +483,6 @@ let is_instance = function
       is_class (IndRef ind)
   | _ -> false
 
-let is_implicit_arg = function
-| Evar_kinds.GoalEvar -> false
-| _ -> true
-  (* match k with *)
-  (*     ImplicitArg (ref, (n, id), b) -> true *)
-  (*   | InternalHole -> true *)
-  (*   | _ -> false *)
-
-
 (* To embed a boolean for resolvability status.
    This is essentially a hack to mark which evars correspond to
    goals and do not need to be resolved when we have nested [resolve_all_evars]
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 1a0b6696..b3170b97 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -77,8 +77,6 @@ val instance_priority : instance -> int option
 val is_class : global_reference -> bool
 val is_instance : global_reference -> bool
 
-val is_implicit_arg : Evar_kinds.t -> bool
-
 (** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 4f88dd86..585f066d 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -10,7 +10,6 @@
 open Names
 open Term
 open Context
-open Evd
 open Environ
 open Constrexpr
 open Globnames
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index dd808771..7982fc85 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -10,7 +10,6 @@ open Loc
 open Names
 open Term
 open Context
-open Evd
 open Environ
 open Constrexpr
 open Globnames
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index c933106d..1f822f1a 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Environ
 open Evd
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 203b1ec8..01e1154e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -673,6 +673,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
               (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
+	| Evar (evk,_ as ev), Evar (evk',_)
+            when not (Evar.Set.mem evk flags.frozen_evars)
+              && Evar.equal evk evk' ->
+	    sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar evk cN) ->
@@ -1673,11 +1677,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | Lambda (_,t,c) ->
 	      (try
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | _ -> error "Match_subterm"))
   in
   try matchrec cl
@@ -1774,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
-	  with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,_,NoOccurrenceFound _) when
+              allow_K ||
+                (* w_unify_to_subterm does not go through evars, so
+                   the next step, which was already in <= 8.4, is
+                   needed at least for compatibility of rewrite *)
+                dependent op t -> (evd,op)
         in
 	  if not allow_K &&
             (* ensure we found a different instance *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 19613c4e..8198db1b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -166,8 +166,15 @@ and nf_whd env whd typ =
       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
+      let tag = btag b in
+      let (tag,ofs) =
+        if tag = Cbytecodes.last_variant_tag then
+	  match whd_val (bfield b 0) with
+	  | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1)
+	  | _ -> assert false
+        else (tag, 0) in
+      let capp,ctyp = construct_of_constr_block env tag typ in
+      let args = nf_bargs env b ofs ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
       let c,typ = constr_type_of_idkey env idkey in
@@ -242,14 +249,14 @@ and nf_args env vargs t =
 	t := subst1 c codom; c) in
   !t,args
 
-and nf_bargs env b t =
+and nf_bargs env b ofs t =
   let t = ref t in
-  let len = bsize b in
+  let len = bsize b - ofs 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
+	let c = nf_val env (bfield b (i+ofs)) dom in
 	t := subst1 c codom; c) in
   args