Imported Upstream version 8.5~beta3+dfsg

37 files changed, 977 insertions, 514 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fcbe90b6..a5a7ace2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1077,7 +1077,7 @@ let rec ungeneralize n ng body =
         let p = prod_applist p [mkRel (n+List.length sign+ng)] in
         it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in
       mkCase (ci,p,c,Array.map2 (fun q c ->
-        let sign,b = decompose_lam_n_assum q c in
+        let sign,b = decompose_lam_n_decls q c in
         it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign)
         ci.ci_cstr_ndecls brs)
   | App (f,args) ->
@@ -1102,7 +1102,8 @@ let rec is_dependent_generalization ng body =
   | Case (ci,p,c,brs) ->
       (* We traverse a split *)
       Array.exists2 (fun q c ->
-        let _,b = decompose_lam_n_assum q c in is_dependent_generalization ng b)
+        let _,b = decompose_lam_n_decls q c in
+        is_dependent_generalization ng b)
         ci.ci_cstr_ndecls brs
   | App (g,args) ->
       (* We traverse an inner generalization *)
@@ -1466,6 +1467,14 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     compile pb
   in
   let sigma = !(pb.evdref) in
+  (* If the "match" was orginally over a variable, as in "match x with
+     O => true | n => n end", we give preference to non-expansion in
+     the default clause (i.e. "match x with O => true | n => n end"
+     rather than "match x with O => true | S p => S p end";
+     computationally, this avoids reallocating constructors in cbv
+     evaluation; the drawback is that it might duplicate the instances
+     of the term to match when the corresponding variable is
+     substituted by a non-evaluated expression *)
   if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then
     (* Try to compile first using non expanded alias *)
     try
@@ -1473,6 +1482,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
       else just_pop ()
     with e when precatchable_exception e ->
     (* Try then to compile using expanded alias *)
+    (* Could be needed in case of dependent return clause *)
     pb.evdref := sigma;
     f expanded expanded_typ
   else
@@ -1480,6 +1490,8 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     try f expanded expanded_typ
     with e when precatchable_exception e ->
     (* Try then to compile using non expanded alias *)
+    (* Could be needed in case of a recursive call which requires to
+       be on a variable for size reasons *)
     pb.evdref := sigma;
     if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
     else just_pop ()
@@ -1668,7 +1680,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
-        let evd,tt = Typing.e_type_of extenv !evdref t in
+        let evd,tt = Typing.type_of extenv !evdref t in
         evdref := evd;
         (t,tt) in
   let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
@@ -1854,10 +1866,10 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
+let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
   let subst, len =
-    List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
+    List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
 	  | Rel n when dependent tm c
@@ -1868,19 +1880,21 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
 		| IsInd (_, IndType(indf,realargs),_) ->
-		    let subst =
-		      if dependent tm c && List.for_all isRel realargs
-		      then (n, 1) :: subst else subst
-		    in
+		    let subst, len =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
 			  | Rel n when dependent arg c ->
 			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
-			(subst, len) realargs)
+			(subst, len) realargs
+		    in
+		    let subst =
+		      if dependent tm c && List.for_all isRel realargs
+		      then (n, len) :: subst else subst
+		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      ([], nar) tomatchs arsign
+      (List.rev tomatchs) arsign ([], nar)
   in
   let rec predicate lift c =
     match kind_of_term c with
@@ -1894,8 +1908,13 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
 	      mkRel (n + nar))
       | _ ->
 	  map_constr_with_binders succ predicate lift c
-  in predicate 0 c
-
+  in
+  assert (len == 0);
+  let p = predicate 0 c in
+  let env' = List.fold_right push_rel_context arsign env in
+  try let sigma' = fst (Typing.type_of env' sigma p) in
+        Some (sigma', p)
+  with e when precatchable_exception e -> None
 
 (* Builds the predicate. If the predicate is dependent, its context is
  * made of 1+nrealargs assumptions for each matched term in an inductive
@@ -1916,11 +1935,13 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
 	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let pred1 =
-          prepare_predicate_from_arsign_tycon loc tomatchs arsign t in
+        let p1 =
+          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	[sigma, pred1; sigma2, pred2]
+	(match p1 with
+	 | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
+	 | None -> [sigma2, pred2])
     | None, _ ->
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
@@ -2014,7 +2035,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
 	  with Not_found -> error_case_not_inductive env 
-	    {uj_val = ty; uj_type = Typing.type_of env !evdref ty}
+	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
 	in
 	let (ind,u), params = dest_ind_family indf in
 	if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind;
@@ -2214,7 +2235,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in
+	 let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
@@ -2392,14 +2413,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
     | None -> let ev = mkExistential env evdref in ev, ev
     | Some t ->
 	let pred = 
-	  try
-	    let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in
-	      (* The tycon may be ill-typed after abstraction. *)
-	    let env' = push_rel_context (context_of_arsign sign) env in
-	      ignore(Typing.sort_of env' evdref pred); pred
-	  with e when Errors.noncritical e ->
-	    let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
-	      lift nar t
+	  match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with
+	  | Some (evd, pred) -> evdref := evd; pred
+	  | None ->
+	     let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
+	       lift nar t
 	in Option.get tycon, pred
   in
   let neqs, arity =
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c421b450..e2bb2d1a 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -78,9 +78,9 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer
 
 (** {6 Lookup functions for coercion paths } *)
 
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
-(** @raise Not_found when no such path exists *)
+(** @raise Not_found in the following functions when no path exists *)
 
+val lookup_path_between_class : cl_index * cl_index -> inheritance_path
 val lookup_path_between : env -> evar_map -> types * types ->
       types * types * inheritance_path
 val lookup_path_to_fun_from : env -> evar_map -> types ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 8ebb8cd2..e61e52c1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		   let evm = !evdref in
 		     (try subco ()
 		      with NoSubtacCoercion ->
-			let typ = Typing.type_of env evm c in
-			let typ' = Typing.type_of env evm c' in
+			let typ = Typing.unsafe_type_of env evm c in
+			let typ' = Typing.unsafe_type_of env evm c' in
 			  (* 			     if not (is_arity env evm typ) then *)
 			  coerce_application typ typ' c c' l l')
 		       (* 			     else subco () *)
@@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	   | x, y when Constr.equal c c' ->
 	       if Int.equal (Array.length l) (Array.length l') then
 		 let evm =  !evdref in
-		 let lam_type = Typing.type_of env evm c in
-		 let lam_type' = Typing.type_of env evm c' in
+		 let lam_type = Typing.unsafe_type_of env evm c in
+		 let lam_type' = Typing.unsafe_type_of env evm c' in
 		   (* 			 if not (is_arity env evm lam_type) then ( *)
 		   coerce_application lam_type lam_type' c c' l l'
 		     (* 			 ) else subco () *)
@@ -345,7 +345,7 @@ let saturate_evd env evd =
   Typeclasses.resolve_typeclasses
     ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
 
-(* appliquer le chemin de coercions p à hj *)
+(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
 let apply_coercion env sigma p hj typ_cl =
   try
     let j,t,evd = 
@@ -367,7 +367,8 @@ let apply_coercion env sigma p hj typ_cl =
   with NoCoercion as e -> raise e
   | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
 
-let inh_app_fun env evd j =
+(* Try to coerce to a funclass; raise NoCoercion if not possible *)
+let inh_app_fun_core env evd j =
   let t = whd_betadeltaiota env evd j.uj_type in
     match kind_of_term t with
     | Prod (_,_,_) -> (evd,j)
@@ -378,7 +379,8 @@ let inh_app_fun env evd j =
       	try let t,p =
 	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
-	with Not_found | NoCoercion when Flags.is_program_mode () ->
+	with Not_found | NoCoercion ->
+          if Flags.is_program_mode () then
 	  try
 	    let evdref = ref evd in
 	    let coercef, t = mu env evdref t in
@@ -386,15 +388,17 @@ let inh_app_fun env evd j =
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
+          else raise NoCoercion
 
+(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
 let inh_app_fun resolve_tc env evd j =
-  try inh_app_fun env evd j
+  try inh_app_fun_core env evd j
   with
-  | Not_found when not resolve_tc 
+  | NoCoercion when not resolve_tc
     || not !use_typeclasses_for_conversion -> (evd, j)
-  | Not_found ->
-    try inh_app_fun env (saturate_evd env evd) j
-    with Not_found -> (evd, j)
+  | NoCoercion ->
+    try inh_app_fun_core env (saturate_evd env evd) j
+    with NoCoercion -> (evd, j)
 
 let inh_tosort_force loc env evd j =
   try
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 161cffa8..5e99521a 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -56,10 +56,6 @@ let warn_bound_meta name =
 let warn_bound_bound name =
   msg_warning (str "Collision between bound variables of name " ++ pr_id name)
 
-let warn_bound_again name =
-  msg_warning (str "Collision between bound variable " ++ pr_id name ++
-    str " and another bound variable of same name.")
-
 let constrain n (ids, m as x) (names, terms as subst) =
   try
     let (ids', m') = Id.Map.find n terms in
@@ -69,32 +65,33 @@ let constrain n (ids, m as x) (names, terms as subst) =
     let () = if Id.Map.mem n names then warn_bound_meta n in
     (names, Id.Map.add n x terms)
 
-let add_binders na1 na2 (names, terms as subst) = match na1, na2 with
-| Name id1, Name id2 ->
-  if Id.Map.mem id1 names then
-    let () = warn_bound_bound id1 in
-    (names, terms)
-  else
-    let names = Id.Map.add id1 id2 names in
-    let () = if Id.Map.mem id1 terms then warn_bound_again id1 in
-    (names, terms)
-| _ -> subst
-
-let rec build_lambda vars stk m = match vars with
+let add_binders na1 na2 binding_vars (names, terms as subst) =
+  match na1, na2 with
+  | Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
+    if Id.Map.mem id1 names then
+      let () = warn_bound_bound id1 in
+      (names, terms)
+    else
+      let names = Id.Map.add id1 id2 names in
+      let () = if Id.Map.mem id1 terms then warn_bound_meta id1 in
+      (names, terms)
+  | _ -> subst
+
+let rec build_lambda vars ctx m = match vars with
 | [] ->
-  let len = List.length stk in
+  let len = List.length ctx in
   lift (-1 * len) m
 | n :: vars ->
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
-  let len = List.length stk in
+  let len = List.length ctx in
   let init i =
     if i < pred n then mkRel (i + 2)
     else if Int.equal i (pred n) then mkRel 1
     else mkRel (i + 1)
   in
   let m = substl (List.init len init) m in
-  let pre, suf = List.chop (pred n) stk in
+  let pre, suf = List.chop (pred n) ctx in
   match suf with
   | [] -> assert false
   | (_, na, t) :: suf ->
@@ -108,21 +105,21 @@ let rec build_lambda vars stk m = match vars with
     let m = mkLambda (na, t, m) in
     build_lambda vars (pre @ suf) m
 
-let rec extract_bound_aux k accu frels stk = match stk with
+let rec extract_bound_aux k accu frels ctx = match ctx with
 | [] -> accu
-| (na1, na2, _) :: stk ->
+| (na1, na2, _) :: ctx ->
   if Int.Set.mem k frels then
     begin match na1 with
     | Name id ->
       let () = assert (match na2 with Anonymous -> false | Name _ -> true) in
       let () = if Id.Set.mem id accu then raise PatternMatchingFailure in
-      extract_bound_aux (k + 1) (Id.Set.add id accu) frels stk
+      extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx
     | Anonymous -> raise PatternMatchingFailure
     end
-  else extract_bound_aux (k + 1) accu frels stk
+  else extract_bound_aux (k + 1) accu frels ctx
 
-let extract_bound_vars frels stk =
-  extract_bound_aux 1 Id.Set.empty frels stk
+let extract_bound_vars frels ctx =
+  extract_bound_aux 1 Id.Set.empty frels ctx
 
 let dummy_constr = mkProp
 
@@ -134,20 +131,20 @@ let make_renaming ids = function
   end
 | _ -> dummy_constr
 
-let merge_binding allow_bound_rels stk n cT subst =
-  let c = match stk with
+let merge_binding allow_bound_rels ctx n cT subst =
+  let c = match ctx with
   | [] -> (* Optimization *)
     ([], cT)
   | _ ->
     let frels = free_rels cT in
     if allow_bound_rels then
-      let vars = extract_bound_vars frels stk in
+      let vars = extract_bound_vars frels ctx in
       let ordered_vars = Id.Set.elements vars in
       let rename binding = make_renaming ordered_vars binding in
-      let renaming = List.map rename stk in
+      let renaming = List.map rename ctx in
       (ordered_vars, substl renaming cT)
     else
-      let depth = List.length stk in
+      let depth = List.length ctx in
       let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in
       if depth < min_elt then
         ([], lift (- depth) cT)
@@ -155,7 +152,8 @@ let merge_binding allow_bound_rels stk n cT subst =
   in
   constrain n c subst
       
-let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
+let matches_core env sigma convert allow_partial_app allow_bound_rels
+    (binding_vars,pat) c =
   let convref ref c = 
     match ref, kind_of_term c with
     | VarRef id, Var id' -> Names.id_eq id id'
@@ -168,7 +166,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	    is_conv env sigma c' c
        else false)
   in
-  let rec sorec stk env subst p t =
+  let rec sorec ctx env subst p t =
     let cT = strip_outer_cast t in
     match p,kind_of_term cT with
       | PSoApp (n,args),m ->
@@ -181,11 +179,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
         let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
         let frels = free_rels cT in
         if Int.Set.subset frels relset then
-          constrain n ([], build_lambda relargs stk cT) subst
+          constrain n ([], build_lambda relargs ctx cT) subst
         else
           raise PatternMatchingFailure
 
-      | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst
+      | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst
 
       | PMeta None, m -> subst
 
@@ -203,10 +201,10 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 
       | PSort (GType _), Sort (Type _) -> subst
 
-      | PApp (p, [||]), _ -> sorec stk env subst p t
+      | PApp (p, [||]), _ -> sorec ctx env subst p t
 
       | PApp (PApp (h, a1), a2), _ ->
-          sorec stk env subst (PApp(h,Array.append a1 a2)) t
+          sorec ctx env subst (PApp(h,Array.append a1 a2)) t
 
       | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
          (let diff = Array.length args2 - Array.length args1 in
@@ -216,13 +214,13 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
             let subst =
               match meta with
               | None -> subst
-              | Some n -> merge_binding allow_bound_rels stk n c subst in
-            Array.fold_left2 (sorec stk env) subst args1 args22
+              | Some n -> merge_binding allow_bound_rels ctx n c subst in
+            Array.fold_left2 (sorec ctx env) subst args1 args22
           else (* Might be a projection on the right *)
 	    match kind_of_term c2 with
 	    | Proj (pr, c) when not (Projection.unfolded pr) ->
 	      (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
-		     sorec stk env subst p term
+		     sorec ctx env subst p term
 	       with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 	    | _ -> raise PatternMatchingFailure)
 	   
@@ -233,15 +231,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	  raise PatternMatchingFailure
 	| PProj (pr1,c1), Proj (pr,c) ->
 	  if Projection.equal pr1 pr then 
-	    try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2
+	    try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
 	    with Invalid_argument _ -> raise PatternMatchingFailure
 	  else raise PatternMatchingFailure
 	| _, Proj (pr,c) when not (Projection.unfolded pr) ->
 	  (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
-		 sorec stk env subst p term
+		 sorec ctx env subst p term
 	   with Retyping.RetypeError _ -> raise PatternMatchingFailure)	    
 	| _, _ ->
-          try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
+          try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2
           with Invalid_argument _ -> raise PatternMatchingFailure)
 	  
       | PApp (PRef (ConstRef c1), _), Proj (pr, c2) 
@@ -250,37 +248,37 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	
       | PApp (c, args), Proj (pr, c2) ->
 	(try let term = Retyping.expand_projection env sigma pr c2 [] in
-	       sorec stk env subst p term
+	       sorec ctx env subst p term
 	 with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 
       | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
-          sorec stk env subst c1 c2
+          sorec ctx env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env)
-            (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2
+	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
-	  sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env)
-            (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2
+	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
-	  sorec ((na1,na2,t2)::stk) (Environ.push_rel (na2,Some c2,t2) env)
-            (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2
+	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (na2,Some c2,t2) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
-	  let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in
-	  let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in
-	  let n = rel_context_length ctx in
-          let n' = rel_context_length ctx' in
+	  let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in
+	  let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in
+	  let n = rel_context_length ctx_b2 in
+          let n' = rel_context_length ctx_b2' in
 	  if noccur_between 1 n b2 && noccur_between 1 n' b2' then
-	    let s =
-	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
-	    let s' =
-	      List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in
+            let f l (na,_,t) = (Anonymous,na,t)::l in
+	    let ctx_br = List.fold_left f ctx ctx_b2 in
+	    let ctx_br' = List.fold_left f ctx ctx_b2' in
 	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
-	    sorec s' (Environ.push_rel_context ctx' env)
-	      (sorec s (Environ.push_rel_context ctx env) (sorec stk env subst a1 a2) b1 b2) b1' b2'
+	    sorec ctx_br' (Environ.push_rel_context ctx_b2' env)
+	      (sorec ctx_br (Environ.push_rel_context ctx_b2 env)
+                 (sorec ctx env subst a1 a2) b1 b2) b1' b2'
           else
             raise PatternMatchingFailure
 
@@ -301,9 +299,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
 	    (* (ind,j+1) is normally known to be a correct constructor
 	       and br2 a correct match over the same inductive *)
 	    assert (j < n2);
-	    sorec stk env subst c br2.(j)
+	    sorec ctx env subst c br2.(j)
 	  in
-	  let chk_head = sorec stk env (sorec stk env subst a1 a2) p1 p2 in
+	  let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
 	  List.fold_left chk_branch chk_head br1
 
       |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
@@ -319,7 +317,8 @@ let matches_core_closed env sigma convert allow_partial_app pat c =
 
 let extended_matches env sigma = matches_core env sigma false true true
 
-let matches env sigma pat c = snd (matches_core_closed env sigma false true pat c)
+let matches env sigma pat c =
+  snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c)
 
 let special_meta = (-1)
 
@@ -343,56 +342,49 @@ let matches_head env sigma pat c =
   matches env sigma pat head
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ env sigma partial_app closed pat c mk_ctx next =
+let authorized_occ env sigma partial_app closed pat c mk_ctx =
   try
     let subst = matches_core_closed env sigma false partial_app pat c in
     if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst)
-    then next ()
-    else mkresult subst (mk_ctx (mkMeta special_meta)) next
-  with PatternMatchingFailure -> next ()
+    then (fun next -> next ())
+    else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
+  with PatternMatchingFailure -> (fun next -> 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
+  let here = authorized_occ env sigma partial_app closed pat c mk_ctx in
+  let next () = match kind_of_term c with
   | Cast (c1,k,c2) ->
       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
+      try_aux [env, c1] next_mk_ctx next
   | Lambda (x,c1,c2) ->
       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, c1); (env', c2)] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      let env' = Environ.push_rel (x,None,c1) env in
+      try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | Prod (x,c1,c2) ->
       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, c1); (env', c2)] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      let env' = Environ.push_rel (x,None,c1) env in
+      try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
       | [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, c1); (env', c2)] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      let env' = Environ.push_rel (x,Some c1,t) env in
+      try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | App (c1,lc) ->
-      let next () =
         let topdown = true in
         if partial_app then
           if topdown then
@@ -421,45 +413,40 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
           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) ->
       let next_mk_ctx = function
-      | [] -> assert false
-      | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
+      | _ -> assert false
       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
+      let sub = (env, c1) :: (env, hd) :: subargs env lc in
+      try_aux sub next_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 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
+    try_aux sub next_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 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
+    try_aux sub next_mk_ctx next
   | Proj (p,c') ->
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
-    let next () = 
       if partial_app then
 	try 
 	  let term = Retyping.expand_projection env sigma p c' [] in
 	    aux env term mk_ctx next
 	with Retyping.RetypeError _ -> next ()
       else
-      try_aux [env, c'] next_mk_ctx next in
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+      try_aux [env, c'] next_mk_ctx next
   | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
-      authorized_occ env sigma partial_app closed pat c mk_ctx next
+    next ()
+  in
+  here next
 
   (* Tries [sub_match] for all terms in the list *)
   and try_aux lc mk_ctx next =
@@ -476,10 +463,10 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
   let result () = aux env c (fun x -> x) lempty in
   IStream.thunk result
 
-let match_subterm env sigma pat c = sub_match env sigma pat c
+let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c
 
 let match_appsubterm env sigma pat c = 
-  sub_match ~partial_app:true env sigma pat c
+  sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c
 
 let match_subterm_gen env sigma app pat c = 
   sub_match ~partial_app:app env sigma pat c
@@ -493,11 +480,12 @@ let is_matching_head env sigma pat c =
   with PatternMatchingFailure -> false
 
 let is_matching_appsubterm ?(closed=true) env sigma pat c =
+  let pat = (Id.Set.empty,pat) in
   let results = sub_match ~partial_app:true ~closed env sigma pat c in
   not (IStream.is_empty results)
 
-let matches_conv env sigma c p =
-  snd (matches_core_closed env sigma true false c p)
+let matches_conv env sigma p c =
+  snd (matches_core_closed env sigma true false (Id.Set.empty,p) c)
 
 let is_matching_conv env sigma pat n =
   try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 67854a89..b9dcb0af 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -41,7 +41,8 @@ val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
    variables or metavariables have the same name, the metavariable,
    or else the rightmost bound variable, takes precedence *)
 val extended_matches :
-  env -> Evd.evar_map -> constr_pattern -> constr -> bound_ident_map * extended_patvar_map
+  env -> Evd.evar_map -> Tacexpr.binding_bound_vars * constr_pattern ->
+  constr -> bound_ident_map * extended_patvar_map
 
 (** [is_matching pat c] just tells if [c] matches against [pat] *)
 val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool
@@ -72,8 +73,10 @@ val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_
 val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
 
 (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
-val match_subterm_gen : env -> Evd.evar_map -> bool (** true = with app context *) ->
-   constr_pattern -> constr -> matching_result IStream.t
+val match_subterm_gen : env -> Evd.evar_map ->
+  bool (** true = with app context *) ->
+  Tacexpr.binding_bound_vars * constr_pattern -> constr ->
+  matching_result IStream.t
 
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
    against [pat] taking partial subterms into consideration *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 28fb8cbe..b5228094 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -276,6 +276,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
     match kind_of_term c with
     | Case (ci,p,c,cl) when
         eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
+        && not (Int.equal (Array.length cl) 0)
 	&& (* don't contract if p dependent *)
 	computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
 	let clauses = build_tree na isgoal e ci cl in
@@ -301,7 +302,7 @@ and contract_branch isgoal e (cdn,can,mkpat,b) =
 let is_nondep_branch c l =
   try
     (* FIXME: do better using tags from l *)
-    let sign,ccl = decompose_lam_n_assum (List.length l) c in
+    let sign,ccl = decompose_lam_n_decls (List.length l) c in
     noccur_between 1 (rel_context_length sign) ccl
   with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
@@ -400,7 +401,7 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
+       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -412,7 +413,7 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
+  GType (Some (dl, Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
 
 let detype_instance sigma l = 
   if Univ.Instance.is_empty l then None
@@ -512,7 +513,7 @@ let rec detype flags avoid env sigma t =
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
-          (Array.map_to_list (fun c -> (Id.of_string "A",c)) cl)
+          (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
       in
         GEvar (dl,id,
                List.map (on_snd (detype flags avoid env sigma)) l)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f388f900..bb07bf05 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -201,13 +201,6 @@ let ise_and evd l =
 	| UnifFailure _ as x -> x in
   ise_and evd l
 
-(* This function requires to get the outermost arguments first.  It is
-   a fold_right for backward compatibility.
-
-   It tries to unify the suffix of 2 lists element by element and if
-   it reaches the end of a list, it returns the remaining elements in
-   the other list if there are some.
-*)
 let ise_exact ise x1 x2 =
   match ise x1 x2 with
   | None, out -> out
@@ -559,13 +552,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
     | MaybeFlexible v1, MaybeFlexible v2 -> begin
         match kind_of_term term1, kind_of_term term2 with
-        | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
+        | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
         let f1 i =
           ise_and i
 	    [(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
+               let na = Nameops.name_max na1 na2 in
 	       evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
@@ -673,13 +667,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     end
 
     | Rigid, Rigid when isLambda term1 && isLambda term2 ->
-        let (na,c1,c'1) = destLambda term1 in
-        let (_,c2,c'2) = destLambda term2 in
+        let (na1,c1,c'1) = destLambda term1 in
+        let (na2,c2,c'2) = destLambda term2 in
         assert app_empty;
         ise_and evd
           [(fun i -> evar_conv_x ts env i CONV c1 c2);
            (fun i ->
 	     let c = nf_evar i c1 in
+             let na = Nameops.name_max na1 na2 in
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
@@ -733,12 +728,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
                UnifFailure (evd,UnifUnivInconsistency p)
 	     | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
 
-	| Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
+	| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
             ise_and evd
               [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
-	         evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
+                 let na = Nameops.name_max n1 n2 in
+	         evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
 	    if Int.equal x1 x2 then
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bfd19c6c..35bc1de5 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -42,21 +42,20 @@ let get_polymorphic_positions f =
         templ.template_param_levels)
   | _ -> assert false
 
-(**
-   forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed
-   hd ?A (l : list t) -> A = t
+let refresh_level evd s =
+  match Evd.is_sort_variable evd s with
+  | None -> true
+  | Some l -> not (Evd.is_flexible_level evd l)
 
-*)
 let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
   let evdref = ref evd in
   let modified = ref false in
-  let rec refresh dir t = 
+  let rec refresh status dir t = 
     match kind_of_term t with
     | Sort (Type u as s) when
       (match Univ.universe_level u with
-      | None -> true 
-      | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) ->
-    let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in
+      | None -> true
+      | Some l -> not onlyalg && refresh_level evd s) ->
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
       if dir then set_leq_sort env !evdref s' s
@@ -64,11 +63,11 @@ 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 status dir v)
     | _ -> t
   (** Refresh the types of evars under template polymorphic references *)
   and refresh_term_evars onevars top t =
-    match kind_of_term t with
+    match kind_of_term (whd_evar !evdref t) with
     | App (f, args) when is_template_polymorphic env f ->
       let pos = get_polymorphic_positions f in
 	refresh_polymorphic_positions args pos
@@ -77,7 +76,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
       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
+      let ty' = refresh univ_flexible true evi.evar_concl in
 	if !modified then 
 	  evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
 	else ()
@@ -99,7 +98,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     if isArity t then
       (match pbty with
       | None -> t
-      | Some dir -> refresh dir t)
+      | Some dir -> refresh univ_rigid dir t)
     else (refresh_term_evars false true t; t)
   in
     if !modified then !evdref, t' else !evdref, t
@@ -107,6 +106,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
 let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
   let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
     refresh_universes (Some false) env sigma ty
+		      
 
 (************************)
 (* Unification results  *)
@@ -127,6 +127,34 @@ let add_conv_oriented_pb ?(tail=true) (pbty,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
 
+(* We retype applications to ensure the universe constraints are collected *)
+
+exception IllTypedInstance of env * types * types
+
+let recheck_applications conv_algo env evdref t =
+  let rec aux env t =
+    match kind_of_term t with
+    | App (f, args) ->
+       let () = aux env f in
+       let fty = Retyping.get_type_of env !evdref f in
+       let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
+       let rec aux i ty =
+	 if i < Array.length argsty then
+	 match kind_of_term (whd_betadeltaiota env !evdref ty) with
+	 | Prod (na, dom, codom) ->
+	    (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
+	     | Success evd -> evdref := evd;
+			     aux (succ i) (subst1 args.(i) codom)
+	     | UnifFailure (evd, reason) ->
+		Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
+	 | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
+       else ()
+     in aux 0 fty
+    | _ ->
+       iter_constr_with_full_binders (fun d env -> push_rel d env) aux env t
+  in aux env t
+
+	  
 (*------------------------------------*
  * Restricting existing evars         *
  *------------------------------------*)
@@ -157,6 +185,7 @@ let restrict_evar_key evd evk filter candidates =
     end
 
 (* Restrict an applied evar and returns its restriction in the same context *)
+(* (the filter is assumed to be at least stronger than the original one) *)
 let restrict_applied_evar evd (evk,argsv) filter candidates =
   let evd,newevk = restrict_evar_key evd evk filter candidates in
   let newargsv = match filter with
@@ -693,7 +722,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
     (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
     (* projectable on [y] *)
       if with_evars then
-        let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
+        let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in
+        let idcl' = List.filter f idcl in
         match idcl' with
         | [c,_,id] ->
           begin
@@ -885,6 +915,9 @@ let filter_candidates evd evk filter candidates_update =
       else
         UpdateWith l'
 
+(* Given a filter refinement for the evar [evk], restrict it so that
+   dependencies are preserved *)
+
 let closure_of_filter evd evk = function
   | None -> None
   | Some filter ->
@@ -892,8 +925,11 @@ let closure_of_filter evd evk = function
   let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
   let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in
   let newfilter = Filter.map_along test filter (evar_context evi) in
+  (* Now ensure that restriction is at least what is was originally *)
+  let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in
   if Filter.equal newfilter (evar_filter evi) then None else Some newfilter
 
+(* The filter is assumed to be at least stronger than the original one *)
 let restrict_hyps evd evk filter candidates =
     (* What to do with dependencies?
        Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
@@ -1099,8 +1135,6 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e
   else
     raise (CannotProject (evd,ev1'))
 
-exception IllTypedInstance of env * types * types
-
 let check_evar_instance evd evk1 body conv_algo =
   let evi = Evd.find evd evk1 in
   let evenv = evar_env evi in
@@ -1114,10 +1148,19 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
+let update_evar_source ev1 ev2 evd =
+  let loc, evs2 = evar_source ev2 evd in
+  match evs2 with
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) ->
+     let evi = Evd.find evd ev1 in
+     Evd.add evd ev1 {evi with evar_source = loc, evs2}
+  | _ -> evd
+  
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
     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
+    let evd' = update_evar_source (fst (destEvar body)) evk2 evd' in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
@@ -1129,8 +1172,8 @@ let preferred_orientation evd evk1 evk2 =
   let _,src2 = (Evd.find_undefined evd evk2).evar_source in
   (* This is a heuristic useful for program to work *)
   match src1,src2 with
-  | Evar_kinds.QuestionMark _, _ -> true
-  | _,Evar_kinds.QuestionMark _ -> false
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true
+  | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false
   | _ -> true
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
@@ -1231,12 +1274,24 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
       | [c,evd] ->
           (* solve_candidates might have been called recursively in the mean *)
           (* time and the evar been solved by the filtering process *)
-          if Evd.is_undefined evd evk then Evd.define evk c evd else evd
+         if Evd.is_undefined evd evk then
+	   let evd' = Evd.define evk c evd in
+	     check_evar_instance evd' evk c conv_algo
+	 else evd
       | l when List.length l < List.length l' ->
           let candidates = List.map fst l in
           restrict_evar evd evk None (UpdateWith candidates)
       | l -> evd
 
+let occur_evar_upto_types sigma n c =
+  let rec occur_rec c = match kind_of_term c with
+    | Evar (sp,_) when Evar.equal sp n -> raise Occur
+    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e);
+		occur_rec (existential_type sigma e)
+    | _ -> iter_constr occur_rec c
+  in
+  try occur_rec c; false with Occur -> true
+
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
@@ -1396,10 +1451,10 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
               evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates);
               evar'')
         | None ->
-          (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
-            map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
-              imitate envk t in
-
+           (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
+	   map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
+					imitate envk t
+  in
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
@@ -1418,9 +1473,13 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
   in
   let body =
     if fast rhs then nf_evar evd rhs
-    else imitate (env,0) rhs
- in (!evdref,body)
-
+    else
+      let t' = imitate (env,0) rhs in
+	if !progress then
+	  (recheck_applications conv_algo (evar_env evi) evdref t'; t')
+	else t'
+  in (!evdref,body)
+     
 (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
  * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
  * [define] tries to find an instance lhs such that
@@ -1445,7 +1504,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
     if occur_meta body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar evk body then raise (OccurCheckIn (evd',body));
+    if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 201a16eb..b27803bd 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -525,7 +525,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
 let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
-     the contexts of the evars occuring in evi *)
+     the contexts of the evars occurring in evi *)
   let terms =
     List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
   let nhyps =
@@ -713,9 +713,10 @@ let define_pure_evar_as_product evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
-  let concl = whd_evar evd evi.evar_concl in
+  let concl = whd_betadeltaiota evenv evd evi.evar_concl in
   let s = destSort concl in
-  let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+  let evd1,(dom,u1) =
+    new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
@@ -724,8 +725,9 @@ let define_pure_evar_as_product evd evk =
        (* Impredicative product, conclusion must fall in [Prop]. *)
         new_evar newenv evd1 concl ~src ~filter
       else
+	let status = univ_flexible_alg in
 	let evd3, (rng, srng) =
-	  new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
+	  new_type_evar newenv evd1 status ~src ~filter in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
 	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
 	  evd3, rng
@@ -757,7 +759,7 @@ let define_evar_as_product evd (evk,args) =
 let define_pure_evar_as_lambda env evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let typ = whd_betadeltaiota env evd (evar_concl evi) in
+  let typ = whd_betadeltaiota evenv evd (evar_concl evi) in
   let evd1,(na,dom,rng) = match kind_of_term typ with
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
@@ -795,8 +797,10 @@ let define_evar_as_sort env evd (ev,args) =
   let evd, u = new_univ_variable univ_rigid evd in
   let evi = Evd.find_undefined evd ev in 
   let s = Type u in
+  let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
+  let sort = destSort concl in
   let evd' = Evd.define ev (mkSort s) evd in
-    Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s
+  Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
 
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
@@ -844,6 +848,25 @@ let subterm_source evk (loc,k) =
   (loc,Evar_kinds.SubEvar evk)
 
 
-(** Term exploration up to isntantiation. *)
+(** Term exploration up to instantiation. *)
 let kind_of_term_upto sigma t =
   Constr.kind (Reductionops.whd_evar sigma t)
+
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+let eq_constr_univs_test sigma1 sigma2 t u =
+  (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
+  let open Evd in
+  let b, c =
+    Universes.eq_constr_univs_infer_with
+      (fun t -> kind_of_term_upto sigma1 t)
+      (fun u -> kind_of_term_upto sigma2 u)
+      (universes sigma2) t u
+  in
+  if b then
+    try let _ = add_universe_constraints sigma2 c in true
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> false
+  else false
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 49036798..f1d94b0a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -206,6 +206,13 @@ val flush_and_check_evars :  evar_map -> constr -> constr
     value of [e] in [sigma] is (recursively) used. *)
 val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
 
+(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
+    [u] up to existential variable instantiation and equalisable
+    universes. The term [t] is interpreted in [sigma1] while [u] is
+    interpreted in [sigma2]. The universe constraints in [sigma2] are
+    assumed to be an extention of those in [sigma1]. *)
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bf519fb7..4a9466f4 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -277,15 +277,14 @@ end
 type evar_universe_context = 
  { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
    uctx_local : Univ.universe_context_set; (** The local context of variables *)
-    uctx_univ_variables : Universes.universe_opt_subst;
-      (** The local universes that are unification variables *)
-    uctx_univ_algebraic : Univ.universe_set; 
-    (** The subset of unification variables that
-	can be instantiated with algebraic universes as they appear in types 
-	and universe instances only. *)
-    uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
-    uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
-  }
+   uctx_univ_variables : Universes.universe_opt_subst;
+   (** The local universes that are unification variables *)
+   uctx_univ_algebraic : Univ.universe_set; 
+   (** The subset of unification variables that can be instantiated with
+	algebraic universes as they appear in inferred types only. *)
+   uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
+   uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+ }
   
 let empty_evar_universe_context = 
   { uctx_names = UNameMap.empty, Univ.LMap.empty;
@@ -310,6 +309,12 @@ let union_evar_universe_context ctx ctx' =
   else
     let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
     let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
+    let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
+			       (Univ.ContextSet.levels ctx.uctx_local) in
+    let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+    let declarenew g =
+      Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+    in
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
 	uctx_local = local;
@@ -317,12 +322,12 @@ let union_evar_universe_context ctx ctx' =
 	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
 	uctx_univ_algebraic = 
 	  Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
-	uctx_initial_universes = ctx.uctx_initial_universes;
+	uctx_initial_universes = declarenew ctx.uctx_initial_universes;
 	uctx_universes = 
 	  if local == ctx.uctx_local then ctx.uctx_universes
 	  else
 	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      Univ.merge_constraints cstrsr ctx.uctx_universes }
+	      Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
 (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
 (* let union_evar_universe_context =  *)
@@ -330,17 +335,38 @@ let union_evar_universe_context ctx ctx' =
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-let evar_universe_context_set ctx = ctx.uctx_local
+let evar_universe_context_set diff ctx =
+  let initctx = ctx.uctx_local in
+  let cstrs =
+    Univ.LSet.fold
+      (fun l cstrs ->
+       try
+	 match Univ.LMap.find l ctx.uctx_univ_variables with
+	 | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
+	 | None -> cstrs
+       with Not_found | Option.IsNone -> cstrs)
+      (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
+  in
+    Univ.ContextSet.add_constraints cstrs initctx 
+		      
 let evar_universe_context_constraints ctx = snd ctx.uctx_local
 let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
+    
 let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
 let evar_universe_context_subst ctx = ctx.uctx_univ_variables
 
+let add_uctx_names s l (names, names_rev) =
+  (UNameMap.add s l names, Univ.LMap.add l s names_rev)
+
+let evar_universe_context_of_binders b =
+  let ctx = empty_evar_universe_context in
+  let names =
+    List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc)
+		   ctx.uctx_names b
+  in { ctx with uctx_names = names }
+					
 let instantiate_variable l b v =
-  (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *)
-  (* if Univ.univ_depends (Univ.Universe.make l) b then  *)
-  (*   error ("Occur-check in universe variable instantiation") *)
-  (* else *) v := Univ.LMap.add l (Some b) !v
+  v := Univ.LMap.add l (Some b) !v
 
 exception UniversesDiffer
 
@@ -374,7 +400,7 @@ let process_universe_constraints univs vars alg cstrs =
 		  let levels = Univ.Universe.levels l in
 		    Univ.LSet.fold (fun l local ->
 		      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
-			Univ.enforce_eq (Univ.Universe.make l) r local
+			unify_universes fo (Univ.Universe.make l) Universes.UEq r local
 		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
 		      levels local
 		else
@@ -406,7 +432,16 @@ let process_universe_constraints univs vars alg cstrs =
 		      raise UniversesDiffer
 	      in
 	        Univ.enforce_eq_level l' r' local
-           | _, _ (* One of the two is algebraic or global *) -> 
+	    | Inr (l, loc, alg), Inl r
+	    | Inl r, Inr (l, loc, alg) ->
+	       let inst = Univ.univ_level_rem l r r in
+		 if alg then (instantiate_variable l inst vars; local)
+		 else
+		   let lu = Univ.Universe.make l in
+		   if Univ.univ_level_mem l r then
+		     Univ.enforce_leq inst lu local
+		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
@@ -433,7 +468,7 @@ let add_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes }
+      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
 
 (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
@@ -553,7 +588,7 @@ type evar_map = {
   (** Metas *)
   metas      : clbinding Metamap.t;
   (** Interactive proofs *)
-  effects    : Declareops.side_effects;
+  effects    : Safe_typing.private_constants;
   future_goals : Evar.t list; (** list of newly created evars, to be
                                   eventually turned into goals if not solved.*)
   principal_future_goal : Evar.t option; (** if [Some e], [e] must be
@@ -564,6 +599,7 @@ type evar_map = {
                                              name) of the evar which
                                              will be instantiated with
                                              a term containing [e]. *)
+  extras : Store.t;
 }
 
 (*** Lifting primitive from Evar.Map. ***)
@@ -723,7 +759,7 @@ let cmap f evd =
   { evd with
       metas = Metamap.map (map_clb f) evd.metas;
       defn_evars = EvMap.map (map_evar_info f) evd.defn_evars;
-      undf_evars = EvMap.map (map_evar_info f) evd.defn_evars
+      undf_evars = EvMap.map (map_evar_info f) evd.undf_evars
   }
 
 (* spiwack: deprecated *)
@@ -741,16 +777,17 @@ let empty = {
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
-  effects    = Declareops.no_seff;
+  effects    = Safe_typing.empty_private_constants;
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
+  extras = Store.empty;
 }
 
-let from_env ?ctx e = 
-  match ctx with
-  | None -> { empty with universes = evar_universe_context_from e }
-  | Some ctx -> { empty with universes = ctx }
+let from_env e = 
+  { empty with universes = evar_universe_context_from e }
+
+let from_ctx ctx = { empty with universes = ctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
@@ -914,38 +951,6 @@ let evars_of_filtered_evar_info evi =
 	(evars_of_named_context (evar_filtered_context evi)))
 
 (**********************************************************)
-(* Side effects *)
-
-let emit_side_effects eff evd =
-  { evd with effects = Declareops.union_side_effects eff evd.effects; }
-
-let drop_side_effects evd =
-  { evd with effects = Declareops.no_seff; }
-
-let eval_side_effects evd = evd.effects
-
-(* Future goals *)
-let declare_future_goal evk evd =
-  { evd with future_goals = evk::evd.future_goals }
-
-let declare_principal_goal evk evd =
-  match evd.principal_future_goal with
-  | None -> { evd with
-    future_goals = evk::evd.future_goals;
-    principal_future_goal=Some evk; }
-  | Some _ -> Errors.error "Only one main subgoal per instantiation."
-
-let future_goals evd = evd.future_goals
-
-let principal_future_goal evd = evd.principal_future_goal
-
-let reset_future_goals evd =
-  { evd with future_goals = [] ; principal_future_goal=None }
-
-let restore_future_goals evd gls pgl =
-  { evd with future_goals = gls ; principal_future_goal = pgl }
-
-(**********************************************************)
 (* Sort variables *)
 
 type rigid = 
@@ -960,19 +965,56 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = d.universes.uctx_local
 
-let universe_context evd =
-  Univ.ContextSet.to_context evd.universes.uctx_local
+let pr_uctx_level uctx = 
+  let map, map_rev = uctx.uctx_names in 
+    fun l ->
+      try str(Univ.LMap.find l map_rev)
+      with Not_found -> 
+	Universes.pr_with_global_universes l
 
+let universe_context ?names evd =
+  match names with
+  | None -> [], Univ.ContextSet.to_context evd.universes.uctx_local
+  | Some pl ->
+     let levels = Univ.ContextSet.levels evd.universes.uctx_local in
+     let newinst, map, left =
+       List.fold_right
+         (fun (loc,id) (newinst, map, acc) ->
+	  let l =
+	    try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names)
+	    with Not_found ->
+	      user_err_loc (loc, "universe_context",
+			    str"Universe " ++ pr_id id ++ str" is not bound anymore.")
+	  in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
+	 pl ([], [], levels)
+     in
+       if not (Univ.LSet.is_empty left) then
+         let n = Univ.LSet.cardinal left in
+           errorlabstrm "universe_context"
+			(str(CString.plural n "Universe") ++ spc () ++
+			     Univ.LSet.pr (pr_uctx_level evd.universes) left ++
+			     spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
+       else
+	 let inst = Univ.Instance.of_array (Array.of_list newinst) in
+	 let ctx = Univ.UContext.make (inst,
+           Univ.ContextSet.constraints evd.universes.uctx_local)
+	 in map, ctx
+
+let restrict_universe_context evd vars =
+  let uctx = evd.universes in
+  let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in
+    { evd with universes = { uctx with uctx_local = uctx' } }
+						 
 let universe_subst evd =
   evd.universes.uctx_univ_variables
 
-let merge_uctx rigid uctx ctx' =
+let merge_uctx sideff rigid uctx ctx' =
   let open Univ in
-  let uctx = 
+  let levels = ContextSet.levels ctx' in
+  let uctx = if sideff then uctx else
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
-      let levels = ContextSet.levels ctx' in
       let fold u accu =
         if LMap.mem u accu then accu
         else LMap.add u None accu
@@ -983,12 +1025,23 @@ let merge_uctx rigid uctx ctx' =
 	  uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
 	else { uctx with uctx_univ_variables = uvars' }
   in
-  let uctx_local = ContextSet.append ctx' uctx.uctx_local in
-  let uctx_universes = merge_constraints (ContextSet.constraints ctx') uctx.uctx_universes in
-  { uctx with uctx_local; uctx_universes }
+  let uctx_local =
+    if sideff then uctx.uctx_local
+    else ContextSet.append ctx' uctx.uctx_local
+  in
+  let declare g =
+    LSet.fold (fun u g ->
+	       try Univ.add_universe u false g
+	       with Univ.AlreadyDeclared when sideff -> g)
+	      levels g
+  in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare uctx.uctx_universes in
+  let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
+    { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
 
-let merge_context_set rigid evd ctx' = 
-  {evd with universes = merge_uctx rigid evd.universes ctx'}
+let merge_context_set ?(sideff=false) rigid evd ctx' = 
+  {evd with universes = merge_uctx sideff rigid evd.universes ctx'}
 
 let merge_uctx_subst uctx s =
   { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
@@ -999,41 +1052,61 @@ let merge_universe_subst evd subst =
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
-let add_uctx_names s l (names, names_rev) =
-    (UNameMap.add s l names, Univ.LMap.add l s names_rev)
-
-let uctx_new_univ_variable rigid name
+let emit_universe_side_effects eff u =
+  let uctxs = Safe_typing.universes_of_private eff in
+  List.fold_left (merge_uctx true univ_rigid) u uctxs
+        
+let uctx_new_univ_variable rigid name predicative
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
   let ctx' = Univ.ContextSet.add_universe u ctx in
-  let uctx' = 
+  let uctx', pred =
     match rigid with
-    | UnivRigid -> uctx
+    | UnivRigid -> uctx, true
     | UnivFlexible b -> 
       let uvars' = Univ.LMap.add u None uvars in
 	if b then {uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = Univ.LSet.add u avars}
-	else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
+	  uctx_univ_algebraic = Univ.LSet.add u avars}, false
+	else {uctx with uctx_univ_variables = uvars'}, false
+  in
   let names = 
     match name with
     | Some n -> add_uctx_names n u uctx.uctx_names
     | None -> uctx.uctx_names
   in
+  let initial =
+    Univ.add_universe u false uctx.uctx_initial_universes
+  in						     
+  let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-      uctx_universes = Univ.add_universe u uctx.uctx_universes}, u
-
-let new_univ_level_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+		uctx_universes = Univ.add_universe u false uctx.uctx_universes;
+		uctx_initial_universes = initial}
+  in uctx', u
+						     
+let new_univ_level_variable ?name ?(predicative=true) rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?name rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name evd.universes in
+let new_univ_variable ?name ?(predicative=true) rigid evd =
+  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?name rigid d =
-  let (d', u) = new_univ_variable rigid ?name d in
+let new_sort_variable ?name ?(predicative=true) rigid d =
+  let (d', u) = new_univ_variable rigid ?name ~predicative d in
     (d', Type u)
 
+let add_global_univ d u =
+  let uctx = d.universes in
+  let initial =
+    Univ.add_universe u true uctx.uctx_initial_universes
+  in
+  let univs = 
+    Univ.add_universe u true uctx.uctx_universes
+  in
+    { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
+				     uctx_initial_universes = initial;
+				     uctx_universes = univs } }
+      
 let make_flexible_variable evd b u =
   let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in
   let uvars' = Univ.LMap.add u None uvars in
@@ -1050,6 +1123,16 @@ let make_flexible_variable evd b u =
     {evd with universes = {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}}
 
+let make_evar_universe_context e l = 
+  let uctx = evar_universe_context_from e in
+    match l with
+    | None -> uctx
+    | Some us ->
+       List.fold_left
+	 (fun uctx (loc,id) ->
+	  fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx))
+	 uctx us
+    
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
@@ -1213,12 +1296,16 @@ let refresh_undefined_univ_variables uctx =
 	Univ.LMap.add (Univ.subst_univs_level_level subst u) 
           (Option.map (Univ.subst_univs_level_universe subst) v) acc)
       uctx.uctx_univ_variables Univ.LMap.empty
-  in 
+  in
+  let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g)
+				   (Univ.ContextSet.levels ctx') g in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare Univ.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
 	       uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
-	       uctx_universes = Univ.initial_universes;
-	       uctx_initial_universes = uctx.uctx_initial_universes } in
+	       uctx_universes = univs;
+	       uctx_initial_universes = initial } in
     uctx', subst
 
 let refresh_undefined_universes evd =
@@ -1232,8 +1319,7 @@ let normalize_evar_universe_context uctx =
       Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
         uctx.uctx_univ_algebraic
     in
-      if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then 
-        uctx
+      if Univ.ContextSet.equal us' uctx.uctx_local then uctx
       else
 	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
 	let uctx' = 
@@ -1271,9 +1357,18 @@ let add_universe_name evd s l =
 
 let universes evd = evd.universes.uctx_universes
 
+let update_sigma_env evd env =
+  let univs = Environ.universes env in
+  let eunivs =
+    { evd.universes with uctx_initial_universes = univs;
+			 uctx_universes = univs }
+  in
+  let eunivs = merge_uctx true univ_rigid eunivs eunivs.uctx_local in
+  { evd with universes = eunivs }
+
 (* Conversion w.r.t. an evar map and its local universes. *)
 
-let conversion_gen env evd pb t u =
+let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
     Reduction.trans_conv_universes 
@@ -1283,14 +1378,8 @@ let conversion_gen env evd pb t u =
      full_transparent_state ~evars:(existential_opt_value evd) env 
     evd.universes.uctx_universes t u
 
-(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *)
-(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *)
-
-let conversion env d pb t u =
-  conversion_gen env d pb t u; d
-
 let test_conversion env d pb t u =
-  try conversion_gen env d pb t u; true
+  try test_conversion_gen env d pb t u; true
   with _ -> false
 
 let eq_constr_univs evd t u =
@@ -1304,8 +1393,38 @@ let e_eq_constr_univs evdref t u =
   let evd, b = eq_constr_univs !evdref t u in
     evdref := evd; b
 
-let eq_constr_univs_test evd t u =
-  snd (eq_constr_univs evd t u)
+(**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+  { evd with effects = Safe_typing.concat_private eff evd.effects;
+	     universes = emit_universe_side_effects eff evd.universes }
+
+let drop_side_effects evd =
+  { evd with effects = Safe_typing.empty_private_constants; }
+
+let eval_side_effects evd = evd.effects
+
+(* Future goals *)
+let declare_future_goal evk evd =
+  { evd with future_goals = evk::evd.future_goals }
+
+let declare_principal_goal evk evd =
+  match evd.principal_future_goal with
+  | None -> { evd with
+    future_goals = evk::evd.future_goals;
+    principal_future_goal=Some evk; }
+  | Some _ -> Errors.error "Only one main subgoal per instantiation."
+
+let future_goals evd = evd.future_goals
+
+let principal_future_goal evd = evd.principal_future_goal
+
+let reset_future_goals evd =
+  { evd with future_goals = [] ; principal_future_goal=None }
+
+let restore_future_goals evd gls pgl =
+  { evd with future_goals = gls ; principal_future_goal = pgl }
 
 (**********************************************************)
 (* Accessing metas *)
@@ -1323,6 +1442,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   principal_future_goal = evd.principal_future_goal;
+  extras = evd.extras;
 }
 
 let meta_list evd = metamap_to_list evd.metas
@@ -1471,6 +1591,12 @@ let dependent_evar_ident ev evd =
   | (_,Evar_kinds.VarInstance id) -> id
   | _ -> anomaly (str "Not an evar resulting of a dependent binding")
 
+(**********************************************************)
+(* Extra data *)
+
+let get_extra_data evd = evd.extras
+let set_extra_data extras evd = { evd with extras }
+
 (*******************************************************************)
 
 type pending = (* before: *) evar_map * (* after: *) evar_map
@@ -1677,13 +1803,6 @@ let evar_dependency_closure n sigma =
 let has_no_evar sigma =
   EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
 
-let pr_uctx_level uctx = 
-  let map, map_rev = uctx.uctx_names in 
-    fun l ->
-      try str(Univ.LMap.find l map_rev)
-      with Not_found -> 
-	Universes.pr_with_global_universes l
-
 let pr_evd_level evd = pr_uctx_level evd.universes
 
 let pr_evar_universe_context ctx =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fe785a83..5c508419 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -129,10 +129,13 @@ type evar_map
 val empty : evar_map
 (** The empty evar map. *)
 
-val from_env : ?ctx:evar_universe_context -> env -> evar_map
+val from_env : env -> evar_map
 (** The empty evar map with given universe context, taking its initial 
     universes from env. *)
 
+val from_ctx : evar_universe_context -> evar_map
+(** The empty evar map with given universe context *)
+
 val is_empty : evar_map -> bool
 (** Whether an evarmap is empty. *)
 
@@ -258,10 +261,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t
 
 (** {5 Side-effects} *)
 
-val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
+val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map
 (** Push a side-effect into the evar map. *)
 
-val eval_side_effects : evar_map -> Declareops.side_effects
+val eval_side_effects : evar_map -> Safe_typing.private_constants
 (** Return the effects contained in the evar map. *)
 
 val drop_side_effects : evar_map -> evar_map
@@ -310,6 +313,19 @@ val add_universe_constraints : evar_map -> Universes.universe_constraints -> eva
     @raises UniversesDiffer in case a first-order unification fails.
     @raises UniverseInconsistency
 *)
+
+(** {5 Extra data}
+
+  Evar maps can contain arbitrary data, allowing to use an extensible state.
+  As evar maps are theoretically used in a strict state-passing style, such
+  additional data should be passed along transparently. Some old and bug-prone
+  code tends to drop them nonetheless, so you should keep cautious.
+
+*)
+
+val get_extra_data : evar_map -> Store.t
+val set_extra_data : Store.t -> evar_map -> evar_map
+
 (** {5 Enriching with evar maps} *)
 
 type 'a sigma = {
@@ -462,7 +478,7 @@ val univ_flexible_alg : rigid
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set
 val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
 val evar_context_universe_context : evar_universe_context -> Univ.universe_context
 val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
@@ -471,6 +487,11 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
 
+val evar_universe_context_of_binders :
+  Universes.universe_binders -> evar_universe_context
+							    
+val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
+val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map							   
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> string -> Univ.universe_level
 val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
@@ -487,9 +508,11 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+val add_global_univ : evar_map -> Univ.Level.t -> evar_map
+											   
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
@@ -514,7 +537,8 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
 
 val evar_universe_context : evar_map -> evar_universe_context
 val universe_context_set : evar_map -> Univ.universe_context_set
-val universe_context : evar_map -> Univ.universe_context
+val universe_context : ?names:(Id.t located) list -> evar_map ->
+		       (Id.t * Univ.Level.t) list * Univ.universe_context
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> Univ.universes
 
@@ -522,7 +546,7 @@ val universes : evar_map -> Univ.universes
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
 val set_universe_context : evar_map -> evar_universe_context -> evar_map
 
-val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
 val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
 
 val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
@@ -536,6 +560,8 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
 
 val nf_constraints : evar_map -> evar_map
 
+val update_sigma_env : evar_map -> env -> evar_map
+
 (** Polymorphic universes *)
 
 val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
@@ -547,14 +573,11 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map ->
   Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
-  Conversion w.r.t. an evar map: might generate universe unifications 
-  that are kept in the evarmap.
-  Raises [NotConvertible]. *)
-
-val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
+  Conversion w.r.t. an evar map, not unifying universes. See 
+  [Reductionops.infer_conv] for conversion up-to universes. *)
 
 val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
-(** This one forgets about the assignemts of universes. *)
+(** WARNING: This does not allow unification of universes *)
 
 val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
 (** Syntactic equality up to universes, recording the associated constraints *)
@@ -562,10 +585,6 @@ val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
 val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
 (** Syntactic equality up to universes. *)
 
-val eq_constr_univs_test : evar_map -> constr -> constr -> bool
-(** Syntactic equality up to universes, throwing away the (consistent) constraints
-    in case of success. *)
-
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 454d64f0..3a76e8bd 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Names
+open Nameops
 open Globnames
 open Misctypes
 open Glob_term
@@ -183,37 +184,32 @@ let map_glob_constr_left_to_right f = function
 
 let map_glob_constr = map_glob_constr_left_to_right
 
-let fold_glob_constr f acc =
-  let rec fold acc = function
+let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
+
+let fold_glob_constr f acc = function
   | GVar _ -> acc
-  | GApp (_,c,args) -> List.fold_left fold (fold acc c) args
+  | GApp (_,c,args) -> List.fold_left f (f acc c) args
   | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) ->
-      fold (fold acc b) c
+    f (f acc b) c
   | GCases (_,_,rtntypopt,tml,pl) ->
-      List.fold_left fold_pattern
-	(List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml))
-	pl
-    | GLetTuple (_,_,rtntyp,b,c) ->
-	fold (fold (fold_return_type acc rtntyp) b) c
-    | GIf (_,c,rtntyp,b1,b2) ->
-	fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2
-    | GRec (_,_,_,bl,tyl,bv) ->
-	let acc = Array.fold_left
-	  (List.fold_left (fun acc (na,k,bbd,bty) ->
-	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
-	Array.fold_left fold (Array.fold_left fold acc tyl) bv
-    | GCast (_,c,k) ->
-        let r = match k with
-        | CastConv t | CastVM t | CastNative t -> fold acc t | CastCoerce -> acc
-        in
-        fold r c
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
-
-  and fold_pattern acc (_,idl,p,c) = fold acc c
-
-  and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt
-
-  in fold acc
+    let fold_pattern acc (_,idl,p,c) = f acc c in
+    List.fold_left fold_pattern
+      (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml))
+      pl
+  | GLetTuple (_,_,rtntyp,b,c) ->
+    f (f (fold_return_type f acc rtntyp) b) c
+  | GIf (_,c,rtntyp,b1,b2) ->
+    f (f (f (fold_return_type f acc rtntyp) c) b1) b2
+  | GRec (_,_,_,bl,tyl,bv) ->
+    let acc = Array.fold_left
+      (List.fold_left (fun acc (na,k,bbd,bty) ->
+	f (Option.fold_left f acc bbd) bty)) acc bl in
+    Array.fold_left f (Array.fold_left f acc tyl) bv
+  | GCast (_,c,k) ->
+    let acc = match k with
+      | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
+    f acc c
+  | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
@@ -328,6 +324,65 @@ let free_glob_vars  =
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
 
+let add_and_check_ident id set =
+  if Id.Set.mem id set then
+    Pp.(msg_warning
+      (str "Collision between bound variables of name " ++ Id.print id));
+  Id.Set.add id set
+
+let bound_glob_vars =
+  let rec vars bound = function
+    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c ->
+        let bound = name_fold add_and_check_ident na bound in
+        fold_glob_constr vars bound c
+    | GCases (loc,sty,rtntypopt,tml,pl) ->
+	let bound = vars_option bound rtntypopt in
+	let bound =
+          List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
+	List.fold_left vars_pattern bound pl
+    | GLetTuple (loc,nal,rtntyp,b,c) ->
+	let bound = vars_return_type bound rtntyp in
+	let bound = vars bound b in
+	let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
+	vars bound c
+    | GIf (loc,c,rtntyp,b1,b2) ->
+	let bound = vars_return_type bound rtntyp in
+	let bound = vars bound c in
+	let bound = vars bound b1 in
+	vars bound b2
+    | GRec (loc,fk,idl,bl,tyl,bv) ->
+	let bound = Array.fold_right Id.Set.add idl bound in
+	let vars_fix i bound fid =
+	  let bound =
+	    List.fold_left
+	      (fun bound (na,k,bbd,bty) ->
+		 let bound = vars_option bound bbd in
+		 let bound = vars bound bty in
+		 name_fold add_and_check_ident na bound
+	      )
+	      bound
+	      bl.(i)
+	  in
+	  let bound = vars bound tyl.(i) in
+	  vars bound bv.(i)
+	in
+	Array.fold_left_i vars_fix bound idl
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
+    | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
+
+  and vars_pattern bound (loc,idl,p,c) =
+    let bound = List.fold_right add_and_check_ident idl bound in
+    vars bound c
+
+  and vars_option bound = function None -> bound | Some p -> vars bound p
+
+  and vars_return_type bound (na,tyopt) =
+    let bound = name_fold add_and_check_ident na bound in
+    vars_option bound tyopt
+  in
+  fun rt ->
+    vars Id.Set.empty rt
+
 (** Mapping of names in binders *)
 
 (* spiwack: I used a smartmap-style kind of mapping here, because the
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index e514fd52..25746323 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -38,6 +38,7 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
+val bound_glob_vars : glob_constr -> Id.Set.t
 val loc_of_glob_constr : glob_constr -> Loc.t
 
 (** [map_pattern_binders f m c] applies [f] to all the binding names
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d4..cb091f2d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -322,7 +322,8 @@ let instantiate_params t args sign =
 let get_constructor ((ind,u as indu),mib,mip,params) j =
   assert (j <= Array.length mip.mind_consnames);
   let typi = mis_nf_constructor_type (indu,mib,mip) j in
-  let typi = instantiate_params typi params mib.mind_params_ctxt in
+  let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let typi = instantiate_params typi params ctx in
   let (args,ccl) = decompose_prod_assum typi in
   let (_,allargs) = decompose_app ccl in
   let vargs = List.skipn (List.length params) allargs in
@@ -584,6 +585,15 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
         env evdref scl ar.template_level (ctx,ar.template_param_levels) in
       !evdref, mkArity (List.rev ctx,scl)
 
+let type_of_projection_knowing_arg env sigma p c ty =
+  let IndType(pars,realargs) =
+    try find_rectype env sigma ty
+    with Not_found ->
+      raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
+  in
+  let (_,u), pars = dest_ind_family pars in
+  substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+
 (***********************************************)
 (* Guard condition *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7959759a..757599a3 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -126,6 +126,8 @@ val allowed_sorts : env -> inductive -> sorts_family list
 (** Primitive projections *)
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
+val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
+  constr -> types -> types
 
 (** Extract information from an inductive family *)
 
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index a2c97d2c..a0ec1baa 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -30,7 +30,7 @@ let smartmap_cast_type f c =
 let glob_sort_eq g1 g2 = match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
-| GType l1, GType l2 -> List.for_all2 CString.equal l1 l2
+| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2
 | _ -> false
 
 let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 5aca11ae..a88c2e20 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -278,6 +278,7 @@ let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
     (fun (na,c,t) newenv ->
+       let na = named_hd newenv t na in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
        push_rel (Name id,c,t) newenv)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index bd427ecd..de988aa2 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -22,11 +22,6 @@ open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-let evars_of_evar_map evd =
-  { evars_val = Evd.existential_opt_value evd;
-    evars_typ = Evd.existential_type evd;
-    evars_metas = Evd.meta_type evd }
-
 exception Find_at of int
 
 let invert_tag cst tag reloc_tbl =
@@ -58,8 +53,8 @@ let find_rectype_a env c =
 
 (* Instantiate inductives and parameters in constructor type *)
 
-let type_constructor mind mib typ params = 
-  let s = ind_subst mind mib Univ.Instance.empty (* FIXME *)in
+let type_constructor mind mib u typ params =
+  let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let nparams = Array.length params in
   if Int.equal nparams 0 then ctyp
@@ -73,13 +68,13 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   let params = Array.sub allargs 0 nparams in
   try
     if const then
-      let ctyp = type_constructor mind mib (mip.mind_nf_lc.(0)) params in
+      let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
       retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp
     else
       raise Not_found
   with Not_found ->
   let i = invert_tag const tag mip.mind_reloc_tbl in
-  let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in
+  let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in
   (mkApp(mkConstructU((ind,i),u), params), ctyp)
  
 
@@ -95,12 +90,12 @@ let construct_of_constr_const env tag typ =
 
 let construct_of_constr_block = construct_of_constr false
 
-let build_branches_type env (mind,_ as _ind) mib mip params dep p =
+let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
   let rtbl = mip.mind_reloc_tbl in
   (* [build_one_branch i cty] construit le type de la ieme branche (commence
      a 0) et les lambda correspondant aux realargs *)
   let build_one_branch i cty =
-    let typi = type_constructor mind mib cty params in
+    let typi = type_constructor mind mib u cty params in
     let decl,indapp = Reductionops.splay_prod env Evd.empty typi in
     let decl_with_letin,_ = decompose_prod_assum typi in
     let ind,cargs = find_rectype_a env indapp in
@@ -150,14 +145,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (sup u1 type0_univ)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
@@ -271,7 +264,7 @@ and nf_atom env atom =
   | Aevar (ev,_) -> mkEvar ev
   | Aproj(p,c) ->
       let c = nf_accu env c in
-	mkProj(Projection.make p false,c)
+	mkProj(Projection.make p true,c)
   | _ -> fst (nf_atom_type env atom)
 
 and nf_atom_type env atom =
@@ -299,7 +292,7 @@ and nf_atom_type env atom =
       let pT = whd_betadeltaiota env pT in
       let dep, p = nf_predicate env ind mip params p pT in
       (* Calcul du type des branches *)
-      let btypes = build_branches_type env (fst ind) mib mip params dep p in
+      let btypes = build_branches_type env (fst ind) mib mip u params dep p in
       (* calcul des branches *)
       let bsw = branch_of_switch (nb_rel env) ans bs in
       let mkbranch i v =
@@ -377,11 +370,17 @@ and  nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_type env v
 
+let evars_of_evar_map sigma =
+  { Nativelambda.evars_val = Evd.existential_opt_value sigma;
+    Nativelambda.evars_typ = Evd.existential_type sigma;
+    Nativelambda.evars_metas = Evd.meta_type sigma }
+
 let native_norm env sigma c ty =  
-  if !Flags.no_native_compiler then
-    error "Native_compute reduction has been disabled"
+  if Coq_config.no_native_compiler then
+    error "Native_compute reduction has been disabled at configure time."
   else
-  let penv = Environ.pre_env env in 
+  let penv = Environ.pre_env env in
+  let sigma = evars_of_evar_map sigma in
   (*
   Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
   Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
@@ -402,3 +401,10 @@ let native_norm env sigma c ty =
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         res
     | _ -> anomaly (Pp.str "Compilation failure") 
+
+let native_conv_generic pb sigma t =
+  Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
+
+let native_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
+  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma)
+    ~catch_incon:true ~pb env sigma t1 t2
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index c854e8c9..03520383 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -12,6 +12,8 @@ open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val evars_of_evar_map : evar_map -> evars
+val native_norm : env -> evar_map -> constr -> types -> constr
 
-val native_norm : env -> evars -> constr -> types -> constr
+(** Conversion with inference of universe constraints *)
+val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 705e594a..fb629d04 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -395,7 +395,9 @@ let rec pat_of_raw metas vars = function
 	| Some p, Some (_,_,nal) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-	| _ -> PMeta None
+        | (None | Some (GHole _)), _ -> PMeta None
+	| Some p, None ->
+            user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0cadffa4..d354a6c3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -99,17 +99,56 @@ let search_guard loc env possible_indexes fixdefs =
 let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = Dyn.create "constr"
 
+(* To force universe name declaration before use *)
+
+let strict_universe_declarations = ref true
+let is_strict_universe_declarations () = !strict_universe_declarations
+
+let _ =
+  Goptions.(declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "strict universe declaration";
+	    optkey   = ["Strict";"Universe";"Declaration"];
+	    optread  = is_strict_universe_declarations;
+	    optwrite = (:=) strict_universe_declarations })
+
+let _ =
+  Goptions.(declare_bool_option
+	  { optsync  = true;
+            optdepr  = false;
+	    optname  = "minimization to Set";
+	    optkey   = ["Universe";"Minimization";"ToSet"];
+	    optread  = Universes.is_set_minimization;
+	    optwrite = (:=) Universes.set_minimization })
+						  
 (** Miscellaneous interpretation functions *)
-let interp_universe_level_name evd s =
+let interp_universe_level_name evd (loc,s) =
   let names, _ = Universes.global_universe_names () in
-  try
-    let id = try Id.of_string s with _ -> raise Not_found in
-      evd, Idmap.find id names
-  with Not_found ->
-    try let level = Evd.universe_of_name evd s in
-	  evd, level
-    with Not_found -> 
-      new_univ_level_variable ~name:s univ_rigid evd
+    if CString.string_contains s "." then
+      match List.rev (CString.split '.' s) with
+      | [] -> anomaly (str"Invalid universe name " ++ str s)
+      | n :: dp -> 
+	 let num = int_of_string n in
+	 let dp = DirPath.make (List.map Id.of_string dp) in
+	 let level = Univ.Level.make dp num in
+	 let evd =
+	   try Evd.add_global_univ evd level
+	   with Univ.AlreadyDeclared -> evd
+	 in evd, level
+    else 
+      try
+	let id =
+	  try Id.of_string s with _ -> raise Not_found in
+	  evd, Idmap.find id names
+      with Not_found ->
+	try let level = Evd.universe_of_name evd s in
+	      evd, level
+	with Not_found -> 
+	  if not (is_strict_universe_declarations ()) then
+  	    new_univ_level_variable ~name:s univ_rigid evd
+	  else user_err_loc (loc, "interp_universe_level_name",
+			     Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe evd = function
   | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
@@ -122,7 +161,7 @@ let interp_universe evd = function
 
 let interp_universe_level evd = function
   | None -> new_univ_level_variable univ_rigid evd
-  | Some s -> interp_universe_level_name evd s
+  | Some (loc,s) -> interp_universe_level_name evd (loc,s)
 
 let interp_sort evd = function
   | GProp -> evd, Prop Null
@@ -270,9 +309,21 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
                            str"It cannot be used in a binder.")
         else n
 
+let ltac_interp_name_env k0 lvar env =
+  (* envhd is the initial part of the env when pretype was called first *)
+  (* (in practice is is probably 0, but we have to grant the
+     specification of pretype which accepts to start with a non empty
+     rel_context) *)
+  (* tail is the part of the env enriched by pretyping *)
+  let n = rel_context_length (rel_context env) - k0 in
+  let ctxt,_ = List.chop n (rel_context env) in
+  let env = pop_rel_context n env in
+  let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in
+  push_rel_context ctxt env
+
 let invert_ltac_bound_name lvar env id0 id =
-  let id = Id.Map.find id lvar.ltac_idents in
-  try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+  let id' = Id.Map.find id lvar.ltac_idents in
+  try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
     errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
 		       str " depends on pattern variable name " ++ pr_id id ++
@@ -285,17 +336,14 @@ let protected_get_type_of env sigma c =
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
-let pretype_id pretype loc env evdref lvar id =
+let pretype_id pretype k0 loc env evdref lvar id =
   let sigma = !evdref in
   (* Look for the binder of [id] *)
   try
-    let id =
-      try Id.Map.find id lvar.ltac_idents
-      with Not_found -> id
-    in
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
+    let env = ltac_interp_name_env k0 lvar env in
     (* Check if [id] is an ltac variable *)
     try
       let (ids,c) = Id.Map.find id lvar.ltac_constrs in
@@ -335,7 +383,8 @@ let evar_kind_of_term sigma c =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_universe_level_name evd = function
+let interp_universe_level_name evd l =
+  match l with
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_universe_level evd s
@@ -374,7 +423,7 @@ let pretype_ref loc evdref env ref us =
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
-    let ty = Typing.type_of env evd c in
+    let ty = Typing.unsafe_type_of env evd c in
       make_judge c ty
 
 let judge_of_Type evd s =
@@ -413,10 +462,10 @@ let is_GHole = function
 
 let evars = ref Id.Map.empty
 
-let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
-  let pretype_type = pretype_type resolve_tc in
-  let pretype = pretype resolve_tc in
+  let pretype_type = pretype_type k0 resolve_tc in
+  let pretype = pretype k0 resolve_tc in
   match t with
   | GRef (loc,ref,u) ->
       inh_conv_coerce_to_tycon loc env evdref
@@ -425,7 +474,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 
   | GVar (loc, id) ->
     inh_conv_coerce_to_tycon loc env evdref
-      (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id)
+      (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
       tycon
 
   | GEvar (loc, id, inst) ->
@@ -436,12 +485,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         with Not_found ->
           user_err_loc (loc,"",str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
-      let args = pretype_instance resolve_tc env evdref lvar loc hyps evk inst in
+      let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = (Retyping.get_judgment_of env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GPatVar (loc,(someta,n)) ->
+    let env = ltac_interp_name_env k0 lvar env in
     let ty =
       match tycon with
       | Some ty -> ty
@@ -450,6 +500,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (loc, k, naming, None) ->
+      let env = ltac_interp_name_env k0 lvar env in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -458,6 +509,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
 
   | GHole (loc, k, _naming, Some arg) ->
+      let env = ltac_interp_name_env k0 lvar env in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -474,12 +526,14 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       | (na,bk,None,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let dcl = (na,None,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+        let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in
+	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
         let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+        let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in
+	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in
     let ctxtv = Array.map (type_bl env empty_rel_context) bl in
     let larj =
       Array.map2
@@ -618,7 +672,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       match evar_kind_of_term !evdref resj.uj_val with
       | App (f,args) ->
         let f = whd_evar !evdref f in
-          if isInd f && is_template_polymorphic env f then
+          if is_template_polymorphic env f then
 	    (* Special case for inductive type applications that must be 
 	       refreshed right away. *)
 	    let sigma = !evdref in
@@ -647,9 +701,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let var = (name,None,j.utj_val) in
     let j' = pretype rng (push_rel var env) evdref lvar c2 in
+    let name = ltac_interp_name lvar name in
     let resj = judge_of_abstraction env (orelse_name name name') j j' in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
@@ -658,7 +712,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let j' = match name with
       | Anonymous ->
         let j = pretype_type empty_valcon env evdref lvar c2 in
@@ -668,6 +721,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         let env' = push_rel_assum var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
+    let name = ltac_interp_name lvar name in
     let resj =
       try
         judge_of_product env name j j'
@@ -689,10 +743,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let var = (name,Some j.uj_val,t) in
     let tycon = lift_tycon 1 tycon in
     let j' = pretype tycon (push_rel var env) evdref lvar c2 in
+    let name = ltac_interp_name lvar name in
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = subst1 j.uj_val j'.uj_type }
 
@@ -712,8 +766,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     if not (Int.equal (List.length nal) cs.cs_nargs) then
       user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
-    let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
-    let na = ltac_interp_name lvar na in
     let fsign, record = 
       match get_projections env indf with
       | None -> List.map2 (fun na (_,c,t) -> (na,c,t))
@@ -729,10 +781,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    (na, c, t) :: aux (n+1) k names l
 	  | [], [] -> []
 	  | _ -> assert false
-	in aux 1 1 (List.rev nal) cs.cs_args, true
-    in
+	in aux 1 1 (List.rev nal) cs.cs_args, true in
     let obj ind p v f =
       if not record then 
+        let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
+        let nal = List.rev nal in
+        let fsign = List.map2 (fun na (_,b,t) -> (na,b,t)) nal fsign in
 	let f = it_mkLambda_or_LetIn f fsign in
 	let ci = make_case_info env (fst ind) LetStyle in
 	  mkCase (ci, p, cj.uj_val,[|f|]) 
@@ -818,7 +872,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	| None ->
 	  let p = match tycon with
 	    | Some ty -> ty
-	    | None -> new_type_evar env evdref loc
+	    | None ->
+              let env = ltac_interp_name_env k0 lvar env in
+              new_type_evar env evdref loc
 	  in
 	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let pred = nf_evar !evdref pred in
@@ -854,9 +910,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       inh_conv_coerce_to_tycon loc env evdref cj tycon
 
   | GCases (loc,sty,po,tml,eqns) ->
-    let (tml,eqns) =
-      Glob_ops.map_pattern_binders (fun na -> ltac_interp_name lvar na) tml eqns
-    in
     Cases.compile_cases loc sty
       ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
       tycon env (* loc *) (po,tml,eqns)
@@ -876,23 +929,20 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 	      if not (occur_existential cty || occur_existential tval) then
-		begin 
-		  try 
-		    ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
-		  with Reduction.NotConvertible -> 
-		    error_actual_type_loc loc env !evdref cj tval 
+		let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in
+		if b then (evdref := evd; cj)
+		else
+		  error_actual_type_loc loc env !evdref cj tval 
                       (ConversionFailed (env,cty,tval))
-		end
 	      else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
-            let evars = Nativenorm.evars_of_evar_map !evdref in
             begin
-              try
-                ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj
-              with Reduction.NotConvertible -> 
+	      let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in
+	      if b then (evdref := evd; cj)
+	      else
                 error_actual_type_loc loc env !evdref cj tval 
                   (ConversionFailed (env,cty,tval))
             end
@@ -903,13 +953,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	  { uj_val = v; uj_type = tval }
     in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
+and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   let f (id,_,t) (subst,update) =
     let t = replace_vars subst t in
     let c, update =
       try
         let c = List.assoc id update in
-        let c = pretype resolve_tc (mk_tycon t) env evdref lvar c in
+        let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
         c.uj_val, List.remove_assoc id update
       with Not_found ->
       try
@@ -929,7 +979,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
   Array.map_of_list snd subst
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type resolve_tc valcon env evdref lvar = function
+and pretype_type k0 resolve_tc valcon env evdref lvar = function
   | GHole (loc, knd, naming, None) ->
       (match valcon with
        | Some v ->
@@ -945,11 +995,12 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 	     { utj_val = v;
 	       utj_type = s }
        | None ->
+           let env = ltac_interp_name_env k0 lvar env in
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
 	     { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
 	       utj_type = s})
   | c ->
-      let j = pretype resolve_tc empty_tycon env evdref lvar c in
+      let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
       let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	match valcon with
@@ -962,13 +1013,14 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let evdref = ref sigma in
+  let k0 = rel_context_length (rel_context env) in
   let c' = match kind with
     | WithoutTypeConstraint ->
-        (pretype flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
+        (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
     | OfType exptyp ->
-	(pretype flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
+	(pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
     | IsType ->
-	(pretype_type flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
+	(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
   in
   process_inference_flags flags env sigma (!evdref,c')
 
@@ -1003,14 +1055,16 @@ let on_judgment f j =
 
 let understand_judgment env sigma c =
   let evdref = ref sigma in
-  let j = pretype true empty_tycon env evdref empty_lvar c in
+  let k0 = rel_context_length (rel_context env) in
+  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   let j = on_judgment (fun c ->
     let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in 
       evdref := evd; c) j
   in j, Evd.evar_universe_context !evdref
 
 let understand_judgment_tcc env evdref c =
-  let j = pretype true empty_tycon env evdref empty_lvar c in
+  let k0 = rel_context_length (rel_context env) in
+  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
     evdref := evd; c) j
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 142b5451..5f0e19cf 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -66,9 +66,12 @@ val all_and_fail_flags : inference_flags
 (** 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
-    unresolved holes as evars and returning the typing contexts of
-    these evars. Work as [understand_gen] for the rest. *)
+(** Generic calls to the interpreter from glob_constr to open_constr;
+    by default, inference_flags tell to use type classes and
+    heuristics (but no external tactic solver hooks), as well as to
+    ensure that conversion problems are all solved and expand evars,
+    but unresolved evars can remain. The difference is in whether the
+    evar_map is modified explicitly or by side-effect. *)
 
 val understand_tcc : ?flags:inference_flags -> env -> evar_map ->
   ?expected_type:typing_constraint -> glob_constr -> open_constr
@@ -92,7 +95,12 @@ val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
   typing_constraint -> glob_constr -> pure_open_constr
 
-(** Standard call to get a constr from a glob_constr, resolving implicit args *)
+(** Standard call to get a constr from a glob_constr, resolving
+    implicit arguments and coercions, and compiling pattern-matching;
+    the default inference_flags tells to use type classes and
+    heuristics (but no external tactic solver hook), as well as to
+    ensure that conversion problems are all solved and that no
+    unresolved evar remains, expanding evars. *)
 
 val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
   env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
@@ -102,12 +110,13 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
 val understand_judgment : env -> evar_map -> 
   glob_constr -> unsafe_judgment Evd.in_evar_universe_context
 
-(** Idem but do not fail on unresolved evars *)
+(** Idem but do not fail on unresolved evars (type cl*)
 val understand_judgment_tcc : env -> evar_map ref ->
   glob_constr -> unsafe_judgment
 
 (** Trying to solve remaining evars and remaining conversion problems
-    with type classes, heuristics, and possibly an external solver *)
+    possibly using type classes, heuristics, external tactic solver
+    hook depending on given flags. *)
 (* For simplicity, it is assumed that current map has no other evars
    with candidate and no other conversion problems that the one in
    [pending], however, it can contain more evars than the pending ones. *)
@@ -115,7 +124,8 @@ val understand_judgment_tcc : env -> evar_map ref ->
 val solve_remaining_evars : inference_flags ->
   env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map
 
-(** Checking evars are all solved and reporting an appropriate error message *)
+(** Checking evars and pending conversion problems are all solved,
+    reporting an appropriate error message *)
 
 val check_evars_are_solved :
   env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
@@ -123,11 +133,11 @@ val check_evars_are_solved :
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
-  bool -> type_constraint -> env -> evar_map ref ->
+  int -> bool -> type_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_judgment
 
 val pretype_type :
-  bool -> val_constraint -> env -> evar_map ref ->
+  int -> bool -> val_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
 val ise_pretype_gen :
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 25d17c7c..a644e3d1 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -3,8 +3,8 @@ Termops
 Namegen
 Evd
 Reductionops
-Vnorm
 Inductiveops
+Vnorm
 Arguments_renaming
 Nativenorm
 Retyping
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6dc0d1f3..7fde7b7a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -190,7 +190,7 @@ let cs_pattern_of_constr t =
 (* Intended to always succeed *)
 let compute_canonical_projections (con,ind) =
   let env = Global.env () in
-  let ctx = Environ.constant_context env con in
+  let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
   let u = Univ.UContext.instance ctx in
   let v = (mkConstU (con,u)) in
   let ctx = Univ.ContextSet.of_context ctx in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dd671f11..0714c93b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1251,9 +1251,6 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
-let sort_cmp cv_pb s1 s2 u = 
-  Reduction.check_sort_cmp_universes cv_pb s1 s2 u
-
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
@@ -1285,16 +1282,18 @@ let sigma_compare_sorts env pb s0 s1 sigma =
   | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
     
-let sigma_compare_instances flex i0 i1 sigma =
+let sigma_compare_instances ~flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
-  with Evd.UniversesDiffer -> raise Reduction.NotConvertible
+  with Evd.UniversesDiffer
+     | Univ.UniverseInconsistency _ ->
+	raise Reduction.NotConvertible
 
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
-    env sigma x y = 
+let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
+    ?(ts=full_transparent_state) env sigma x y =
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1311,14 +1310,23 @@ let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_s
       if b then sigma, true
       else
 	let sigma' = 
-	  Reduction.generic_conv pb false (safe_evar_value sigma) ts 
+	  conv_fun pb ~l2r:false sigma ts
 	    env (sigma, sigma_univ_state) x y in
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
   | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
-    
+
+let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
+      Reduction.generic_conv pb ~l2r (safe_evar_value sigma))
+
+(* This reference avoids always having to link C code with the kernel *)
+let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:full_transparent_state)
+let set_vm_infer_conv f = vm_infer_conv := f
+let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
+  !vm_infer_conv ~pb env t1 t2
+
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1df2a73b..d5a84484 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -251,8 +251,6 @@ type conversion_test = constraints -> constraints
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val sort_cmp : env -> conv_pb -> sorts -> sorts -> universes -> unit
-
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
 val is_fconv : conv_pb -> env ->  evar_map -> constr -> constr -> bool
@@ -266,7 +264,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env ->  evar_map -> constr
  *)
 val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> bool
 
-(** [infer_fconv] Adds necessary universe constraints to the evar map.
+(** [infer_conv] 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.
@@ -274,6 +272,20 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
   env -> evar_map -> constr -> constr -> evar_map * bool
 
+(** Conversion with inference of universe constraints *)
+val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool) -> unit
+val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
+
+
+(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
+conversion function. Used to pretype vm and native casts. *)
+val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
+    (constr, evar_map) Reduction.generic_conversion_function) ->
+  ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
+  evar_map -> constr -> constr -> evar_map * bool
+
 (** {6 Special-Purpose Reduction Functions } *)
 
 val whd_meta : evar_map -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a56861c6..fb552655 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -126,14 +126,11 @@ let retype ?(polyprop=true) sigma =
     | App(f,args) ->
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
-    | Proj (p,c) -> 
-       let Inductiveops.IndType(pars,realargs) =
-	 let ty = type_of env c in
-           try Inductiveops.find_rectype env sigma ty
-           with Not_found -> retype_error BadRecursiveType
-       in
-       let (_,u), pars = dest_ind_family pars in
-	 substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+    | Proj (p,c) ->
+       let ty = type_of env c in
+       (try
+	   Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+	 with Invalid_argument _ -> retype_error BadRecursiveType)
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 372b26aa..48911a5a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1011,8 +1011,8 @@ let contextually byhead occs f env sigma t =
     snd (e_contextually byhead occs f' env sigma t)
 
 (* linear bindings (following pretty-printer) of the value of name in c.
- * n is the number of the next occurence of name.
- * ol is the occurence list to find. *)
+ * n is the number of the next occurrence of name.
+ * ol is the occurrence list to find. *)
 
 let match_constr_evaluable_ref sigma c evref = 
   match kind_of_term c, evref with
@@ -1061,7 +1061,7 @@ let is_projection env = function
 
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
- * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
+ * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
   let unfo nowhere_except_in locs =
@@ -1134,7 +1134,7 @@ let abstract_scheme env (locc,a) (c, sigma) =
 let pattern_occs loccs_trm env sigma c =
   let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in
   try
-    let _ = Typing.type_of env sigma abstr_trm in
+    let _ = Typing.unsafe_type_of env sigma abstr_trm in
       sigma, applist(abstr_trm, List.map snd loccs_trm)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9f04faa8..5a55d47f 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -453,26 +453,29 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_binders g f n acc c = match kind_of_term c with
+let fold_constr_with_full_binders g f n acc c = match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (_,t,c) -> f (g n) (f n acc t) c
-  | Lambda (_,t,c) -> f (g n) (f n acc t) c
-  | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = iterate g (Array.length tl) n in
+      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = iterate g (Array.length tl) n in
+      let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
+let fold_constr_with_binders g f n acc c =
+  fold_constr_with_full_binders (fun _ x -> g x) f n acc c
+
 (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
    subterms of [c]; it carries an extra data [acc] which is processed by [g] at
    each binder traversal; it is not recursive and the order with which
@@ -558,7 +561,7 @@ let free_rels m =
   in
   frec 1 Int.Set.empty m
 
-(* collects all metavar occurences, in left-to-right order, preserving
+(* collects all metavar occurrences, in left-to-right order, preserving
  * repetitions and all. *)
 
 let collect_metas c =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 2552c67e..4581e231 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -84,6 +84,10 @@ val map_constr_with_full_binders :
 val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
+val fold_constr_with_full_binders :
+  (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+    'a -> 'b -> constr -> 'b
+
 val iter_constr_with_full_binders :
   (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
     constr -> unit
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 18e83056..2ef28965 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -370,7 +370,7 @@ let add_instance check inst =
   List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
     (is_local inst) pri poly)
     (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
-       (Global.env ()) Evd.empty inst.is_impl inst.is_pri)
+       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
 
 let rebuild_instance (action, inst) =
   let () = match action with
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c6209cc3..fb5927db 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -270,7 +270,7 @@ let check env evdref c t =
 
 (* Type of a constr *)
 
-let type_of env evd c =
+let unsafe_type_of env evd c =
   let j = execute env (ref evd) c in
     j.uj_type
 
@@ -283,7 +283,7 @@ let sort_of env evdref c =
 
 (* Try to solve the existential variables by typing *)
 
-let e_type_of ?(refresh=false) env evd c =
+let type_of ?(refresh=false) env evd c =
   let evdref = ref evd in
   let j = execute env evdref c in
   (* side-effect on evdref *)
@@ -291,6 +291,15 @@ let e_type_of ?(refresh=false) env evd c =
       Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
     else !evdref, j.uj_type
 
+let e_type_of ?(refresh=false) env evdref c =
+  let j = execute env evdref c in
+  (* side-effect on evdref *)
+    if refresh then
+      let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in
+      let () = evdref := evd in
+      c
+    else j.uj_type
+
 let solve_evars env evdref c =
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1f822f1a..bfae46ff 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -13,12 +13,15 @@ open Evd
 (** This module provides the typing machine with existential variables
     and universes. *)
 
-(** Typecheck a term and return its type *)
-val type_of : env -> evar_map -> constr -> types
+(** Typecheck a term and return its type. May trigger an evarmap leak. *)
+val unsafe_type_of : env -> evar_map -> constr -> types
 
 (** Typecheck a term and return its type + updated evars, optionally refreshing
     universes *)
-val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+
+(** Variant of [type_of] using references instead of state-passing. *)
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map ref -> types -> sorts
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 01e1154e..24e06007 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -93,7 +93,7 @@ let abstract_list_all env evd typ c l =
   let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
   let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
   let evd,typp =
-    try Typing.e_type_of env evd p
+    try Typing.type_of env evd p
     with
     | UserError _ ->
         error_cannot_find_well_typed_abstraction env evd p l None
@@ -676,7 +676,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	| 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)
+            let sigma',b = constr_cmp cv_pb sigma flags cM cN in
+            if b then
+	      sigma',metasubst,evarsubst
+            else
+	      sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar evk cN) ->
@@ -1150,7 +1154,7 @@ let applyHead env evd n c  =
 	  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
+    apprec n c (Typing.unsafe_type_of env evd c) evd
     
 let is_mimick_head ts f =
   match kind_of_term f with
@@ -1528,7 +1532,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      error ("The variable "^(Id.to_string x)^" is already declared.")
+      errorlabstrm "Unification.make_abstraction_core"
+        (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
   in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8198db1b..c4c85a62 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -93,19 +93,6 @@ let construct_of_constr_const env tag typ =
 
 let construct_of_constr_block = construct_of_constr false
 
-let constr_type_of_idkey env idkey =
-  match idkey with
-  | ConstKey cst ->
-    let const_type = Typeops.type_of_constant_in env cst in
-      mkConstU cst, const_type
-  | VarKey id ->
-      let (_,_,ty) = lookup_named id env in
-      mkVar id, ty
-  | RelKey i ->
-      let n = (nb_rel env - i) in
-      let (_,_,ty) = lookup_rel n env in
-      mkRel n, lift n ty
-
 let type_of_ind env (ind, u) =
   type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
 
@@ -164,7 +151,8 @@ and nf_whd env whd typ =
       let t = ta.(i) in
       let _, args = nf_args env vargs t in
       mkApp(cfd,args)
-  | Vconstr_const n -> construct_of_constr_const env n typ
+  | Vconstr_const n ->
+    construct_of_constr_const env n typ
   | Vconstr_block b ->
       let tag = btag b in
       let (tag,ofs) =
@@ -177,24 +165,72 @@ and nf_whd env whd typ =
       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
-      nf_stk env c typ stk
-  | Vatom_stk(Aiddef(idkey,v), stk) ->
-      nf_whd env (whd_stack v stk) typ
-  | Vatom_stk(Aind ind, stk) ->
-      nf_stk env (mkIndU ind) (type_of_ind env ind) stk
-
-and nf_stk env c t stk  =
+      constr_type_of_idkey env idkey stk
+  | Vatom_stk(Aind ((mi,i) as ind), stk) ->
+     let mib = Environ.lookup_mind mi env in
+     let nb_univs =
+       if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes
+       else 0
+     in
+     let mk u =
+       let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
+     in
+     nf_univ_args ~nb_univs mk env stk
+  | Vatom_stk(Atype u, stk) -> assert false
+  | Vuniv_level lvl ->
+    assert false
+
+and nf_univ_args ~nb_univs mk env stk =
+  let u =
+    if Int.equal nb_univs 0 then Univ.Instance.empty
+    else match stk with
+    | Zapp args :: _ ->
+       let inst =
+	 Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i))
+       in
+       Univ.Instance.of_array inst
+    | _ -> assert false
+  in
+  let (t,ty) = mk u in
+  nf_stk ~from:nb_univs env t ty stk
+
+and constr_type_of_idkey env (idkey : Vars.id_key) stk =
+  match idkey with
+  | ConstKey cst ->
+     let cbody = Environ.lookup_constant cst env in
+     let nb_univs =
+       if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes
+       else 0
+     in
+     let mk u =
+       let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)
+     in
+     nf_univ_args ~nb_univs mk env stk
+   | VarKey id ->
+      let (_,_,ty) = lookup_named id env in
+      nf_stk env (mkVar id) ty stk
+  | RelKey i ->
+      let n = (nb_rel env - i) in
+      let (_,_,ty) = lookup_rel n env in
+      nf_stk env (mkRel n) (lift n ty) stk
+
+and nf_stk ?from:(from=0) env c t stk  =
   match stk with
   | [] -> c
   | Zapp vargs :: stk ->
-      let t, args = nf_args env vargs t in
-      nf_stk env (mkApp(c,args)) t stk
+      if nargs vargs >= from then
+	let t, args = nf_args ~from:from env vargs t in
+	nf_stk env (mkApp(c,args)) t stk
+      else
+	let rest = from - nargs vargs in
+	nf_stk ~from:rest env c t stk
   | Zfix (f,vargs) :: stk ->
+      assert (from = 0) ;
       let fa, typ = nf_fix_app env f vargs in
       let _,_,codom = decompose_prod env typ in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
+      assert (from = 0) ;
       let ((mind,_ as ind), u), allargs = find_rectype_a env t in
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
@@ -216,6 +252,11 @@ and nf_stk env c t stk  =
       let tcase = build_case_type dep p realargs c in
       let ci = case_info sw in
       nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+  | Zproj p :: stk ->
+     assert (from = 0) ;
+     let p' = Projection.make p true in
+     let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
+     nf_stk env (mkProj(p',c)) ty stk
 
 and nf_predicate env ind mip params v pT =
   match whd_val v, kind_of_term pT with
@@ -238,14 +279,14 @@ and nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_val env v crazy_type
 
-and nf_args env vargs t =
+and nf_args env vargs ?from:(f=0) t =
   let t = ref t in
-  let len = nargs vargs in
+  let len = nargs vargs - f in
   let args =
     Array.init len
       (fun i ->
 	let _,dom,codom = decompose_prod env !t in
-	let c = nf_val env (arg vargs i) dom in
+	let c = nf_val env (arg vargs (f+i)) dom in
 	t := subst1 c codom; c) in
   !t,args
 
@@ -308,10 +349,11 @@ and nf_cofix env cf =
   mkCoFix (init,(name,cft,cfb))
 
 let cbv_vm env c t  =
-  let transp = transp_values () in
-  if not transp then set_transp_values true;
   let v = Vconv.val_of_constr env c in
-  let c = nf_val env v t in
-  if not transp then set_transp_values false;
-  c
+  nf_val env v t
+
+let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
+  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
+    ~catch_incon:true ~pb env sigma t1 t2
 
+let _ = Reductionops.set_vm_infer_conv vm_infer_conv
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 7dabbc6c..9421b2d8 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -8,7 +8,7 @@
 
 open Term
 open Environ
+open Evd
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr
-