Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.

16 files changed, 348 insertions, 239 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 92bd1e389..b43e2193a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -89,9 +89,6 @@ let list_try_compile f l =
 let force_name =
   let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
 
-let make_judge c ty =
-  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
-
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
 (************************************************************************)
@@ -265,7 +262,7 @@ type 'a pattern_matching_problem =
       mat       : 'a matrix;
       caseloc   : Loc.t;
       casestyle : case_style;
-      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
+      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> EConstr.unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
  * A few functions to infer the inductive type from the patterns instead of *
@@ -366,12 +363,12 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let j = typing_fun tycon env evdref tomatch in
   let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in
   evdref := evd;
-  let typ = EConstr.of_constr (nf_evar !evdref j.uj_type) in
+  let typ = EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr j.uj_type)) in
   let t =
     try try_find_ind env !evdref typ realnames
     with Not_found ->
       unify_tomatch_with_patterns evdref env loc typ pats realnames in
-  (EConstr.of_constr j.uj_val,t)
+  (j.uj_val,t)
 
 let coerce_to_indtype typing_fun evdref env matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
@@ -415,7 +412,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 		let _ = e_cumul pb.env pb.evdref indt typ in
 		current
 	      else
-		EConstr.of_constr (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env)
+		(evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env)
 		  pb.evdref (make_judge current typ) indt).uj_val in
 	    let sigma =  !(pb.evdref) in
 	    (current,try_find_ind pb.env sigma indt names))
@@ -1002,7 +999,7 @@ let adjust_impossible_cases pb pred tomatch submat =
     | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
         if not (Evd.is_defined !(pb.evdref) evk) then begin
 	  let evd, default = use_unit_judge !(pb.evdref) in
-	  pb.evdref := Evd.define evk default.uj_type evd
+	  pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd
         end;
         add_assert_false_case pb tomatch
     | _ ->
@@ -1411,8 +1408,8 @@ and match_current pb (initial,tomatch) =
 	    make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
 	  in
 	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
-	  { uj_val = EConstr.Unsafe.to_constr (applist (case, inst));
-	    uj_type = EConstr.Unsafe.to_constr (prod_applist !(pb.evdref) typ inst) }
+	  { uj_val = applist (case, inst);
+	    uj_type = prod_applist !(pb.evdref) typ inst }
 
 
 (* Building the sub-problem when all patterns are variables. Case
@@ -1429,8 +1426,8 @@ and shift_problem ((current,t),_,na) pb =
        history = pop_history pb.history;
        mat = List.map (push_current_pattern (current,ty)) pb.mat } in
   let j = compile pb in
-  { uj_val = EConstr.Unsafe.to_constr (subst1 current (EConstr.of_constr j.uj_val));
-    uj_type = EConstr.Unsafe.to_constr (subst1 current (EConstr.of_constr j.uj_type)) }
+  { uj_val = subst1 current j.uj_val;
+    uj_type = subst1 current j.uj_type }
 
 (* Building the sub-problem when all patterns are variables,
    non-initial case. Variables which appear as subterms of constructor
@@ -1453,7 +1450,7 @@ and compile_all_variables initial cur pb =
 (* Building the sub-problem when all patterns are variables *)
 and compile_branch initial current realargs names deps pb arsign eqns cstr =
   let sign, pb = build_branch initial current realargs deps names pb arsign eqns cstr in
-  sign, EConstr.of_constr (compile pb).uj_val
+  sign, (compile pb).uj_val
 
 (* Abstract over a declaration before continuing splitting *)
 and compile_generalization pb i d rest =
@@ -1463,8 +1460,8 @@ and compile_generalization pb i d rest =
        tomatch = rest;
        mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in
   let j = compile pb in
-  { uj_val = Term.mkLambda_or_LetIn d j.uj_val;
-    uj_type = Term.mkProd_wo_LetIn d j.uj_type }
+  { uj_val = mkLambda_or_LetIn d j.uj_val;
+    uj_type = mkProd_wo_LetIn d j.uj_type }
 
 (* spiwack: the [initial] argument keeps track whether the alias has
    been introduced by a toplevel branch ([true]) or a deep one
@@ -1482,11 +1479,11 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
     let j = compile pb in
     let sigma = !(pb.evdref) in
     { uj_val =
-        if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) (EConstr.of_constr j.uj_val) <= 1 then
-          EConstr.Unsafe.to_constr (subst1 c (EConstr.of_constr j.uj_val))
+        if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
+          subst1 c j.uj_val
         else
-          EConstr.Unsafe.to_constr (mkLetIn (na,c,t,EConstr.of_constr j.uj_val));
-      uj_type = EConstr.Unsafe.to_constr (subst1 c (EConstr.of_constr j.uj_type)) } in
+          mkLetIn (na,c,t,j.uj_val);
+      uj_type = subst1 c j.uj_type } in
   (* spiwack: when an alias appears on a deep branch, its non-expanded
      form is automatically a variable of the same name. We avoid
      introducing such superfluous aliases so that refines are elegant. *)
@@ -1726,7 +1723,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
         (t,tt) in
   let b = e_cumul env evdref tt (mkSort s) (* side effect *) in
   if not b then anomaly (Pp.str "Build_tycon: should be a type");
-  { uj_val = EConstr.Unsafe.to_constr t; uj_type = EConstr.Unsafe.to_constr tt }
+  { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
  * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return
@@ -1851,7 +1848,7 @@ let build_inversion_problem loc env sigma tms t =
       caseloc   = loc;
       casestyle = RegularStyle;
       typing_function = build_tycon loc env pb_env s subst} in
-  let pred = EConstr.of_constr (compile pb).uj_val in
+  let pred = (compile pb).uj_val in
   (!evdref,pred)
 
 (* Here, [pred] is assumed to be in the context built from all *)
@@ -1905,7 +1902,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 let inh_conv_coerce_to_tycon loc env evdref j tycon =
   match tycon with
     | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j (EConstr.of_constr p) in
+	let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in
           evdref := evd';
           j
     | None -> j
@@ -2029,7 +2026,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
       let evdref = ref sigma in
       let predcclj = typing_fun (mk_tycon (EConstr.mkSort newt)) envar evdref rtntyp in
       let sigma = !evdref in
-      let predccl = EConstr.of_constr (j_nf_evar sigma predcclj).uj_val in
+      let predccl = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr predcclj.uj_val)) in
       [sigma, predccl]
   in
   List.map
@@ -2095,7 +2092,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 !evdref
-	    {uj_val = EConstr.Unsafe.to_constr ty; uj_type = Typing.unsafe_type_of env !evdref ty}
+	    {uj_val = ty; uj_type = EConstr.of_constr (Typing.unsafe_type_of env !evdref ty)}
 	in
 	let (ind,u), params = dest_ind_family indf in
 	let params = List.map EConstr.of_constr params in
@@ -2297,8 +2294,8 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 in
 	 let rhs_env = push_rel_context rhs_rels' env in
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
-	 let bbody = it_mkLambda_or_LetIn (EConstr.of_constr j.uj_val) rhs_rels'
-	 and btype = it_mkProd_or_LetIn (EConstr.of_constr j.uj_type) rhs_rels' 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.type_of env) evdref bbody in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = local_def (Name branch_name, lift !i bbody, lift !i btype) in
@@ -2554,10 +2551,10 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
   let j = compile pb in
     (* We check for unused patterns *)
     List.iter (check_unused_pattern env) matx;
-    let body = it_mkLambda_or_LetIn (applist (EConstr.of_constr j.uj_val, args)) lets in
+    let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
     let j =
-      { uj_val = EConstr.Unsafe.to_constr (it_mkLambda_or_LetIn body tomatchs_lets);
-	uj_type = EConstr.to_constr !evdref tycon; }
+      { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
+	uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); }
     in j
 
 (**************************************************************************)
@@ -2632,7 +2629,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
     let j = compile pb in
 
     (* We coerce to the tycon (if an elim predicate was provided) *)
-    let j = inh_conv_coerce_to_tycon loc env myevdref j (Option.map EConstr.Unsafe.to_constr tycon) in
+    let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in
     evdref := !myevdref;
     j in
 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9016ca5f3..9f26ae9ce 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -8,9 +8,9 @@
 
 open Names
 open Term
-open EConstr
 open Evd
 open Environ
+open EConstr
 open Inductiveops
 open Glob_term
 open Evarutil
@@ -111,11 +111,11 @@ type 'a pattern_matching_problem =
       typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
 
 
-val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
+val compile : 'a pattern_matching_problem -> unsafe_judgment
 
 val prepare_predicate :            Loc.t ->
            (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+            Environ.env -> Evd.evar_map ref -> 'a -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
            (types * tomatch_type) list ->
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ad43bf322..9011186a3 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -319,7 +319,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
   let subst, ctx = Universes.fresh_universe_context_set_instance ctx in
   let c' = Vars.subst_univs_level_constr subst c 
   and t' = Vars.subst_univs_level_constr subst t in
-    (make_judge c' t', b, b'), ctx
+    (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx
 
 (* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 9fb70534f..a1d030f12 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -8,9 +8,9 @@
 
 open Names
 open Term
+open Environ
 open EConstr
 open Evd
-open Environ
 open Mod_subst
 
 (** {6 This is the type of class kinds } *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b9f14aa43..2d4296fe4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -53,16 +53,16 @@ let apply_coercion_args env evd check isproj argl funj =
   let rec apply_rec acc typ = function
     | [] ->
       if isproj then
-	let cst = fst (destConst !evdref (EConstr.of_constr (j_val funj))) in
+	let cst = fst (destConst !evdref (j_val funj)) in
 	let p = Projection.make cst false in
 	let pb = lookup_projection p env in
 	let args = List.skipn pb.Declarations.proj_npars argl in
 	let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
-	  { uj_val = EConstr.Unsafe.to_constr (applist (mkProj (p, hd), tl));
-	    uj_type = EConstr.Unsafe.to_constr typ }
+	  { uj_val = applist (mkProj (p, hd), tl);
+	    uj_type = typ }
       else
-	{ uj_val = EConstr.Unsafe.to_constr (applist (EConstr.of_constr (j_val funj),argl));
-	  uj_type = EConstr.Unsafe.to_constr typ }
+	{ uj_val = applist (j_val funj,argl);
+	  uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
       match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
       | Prod (_,c1,c2) ->
@@ -71,7 +71,7 @@ let apply_coercion_args env evd check isproj argl funj =
         apply_rec (h::acc) (Vars.subst1 h c2) restl
       | _ -> anomaly (Pp.str "apply_coercion_args")
   in
-  let res = apply_rec [] (EConstr.of_constr funj.uj_type) argl in
+  let res = apply_rec [] funj.uj_type argl in
     !evdref, res
 
 (* appliquer le chemin de coercions de patterns p *)
@@ -367,7 +367,7 @@ let apply_coercion env sigma p hj typ_cl =
         (fun (ja,typ_cl,sigma) i ->
 	  let ((fv,isid,isproj),ctx) = coercion_value i in
 	  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-	  let argl = (class_args_of env sigma typ_cl)@[EConstr.of_constr ja.uj_val] in
+	  let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 	  let sigma, jres = 
 	    apply_coercion_args env sigma true isproj argl fv 
 	  in
@@ -375,7 +375,7 @@ let apply_coercion env sigma p hj typ_cl =
 	      { uj_val = ja.uj_val; uj_type = jres.uj_type }
 	     else
 	      jres),
-	    EConstr.of_constr jres.uj_type,sigma)
+	    jres.uj_type,sigma)
       (hj,typ_cl,sigma) p
     in evd, j
   with NoCoercion as e -> raise e
@@ -383,23 +383,23 @@ let apply_coercion env sigma p hj typ_cl =
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =
-  let t = whd_all env evd (EConstr.of_constr j.uj_type) in
+  let t = whd_all env evd j.uj_type in
   let t = EConstr.of_constr t in
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
 	let (evd',t) = Evardefine.define_evar_as_product evd ev in
-	  (evd',{ uj_val = j.uj_val; uj_type = EConstr.Unsafe.to_constr t })
+	  (evd',{ uj_val = j.uj_val; uj_type = t })
     | _ ->
       	try let t,p =
-	  lookup_path_to_fun_from env evd (EConstr.of_constr j.uj_type) in
+	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
 	with Not_found | NoCoercion ->
           if Flags.is_program_mode () then
 	  try
 	    let evdref = ref evd in
 	    let coercef, t = mu env evdref t in
-	    let res = { uj_val = EConstr.Unsafe.to_constr (app_opt env evdref coercef (EConstr.of_constr j.uj_val)); uj_type = EConstr.Unsafe.to_constr t } in
+	    let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
@@ -415,17 +415,23 @@ let inh_app_fun resolve_tc env evd j =
     try inh_app_fun_core env (saturate_evd env evd) j
     with NoCoercion -> (evd, j)
 
+let type_judgment env sigma j =
+  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma j.uj_type)) with
+    | Sort s -> {utj_val = j.uj_val; utj_type = s }
+    | _ -> error_not_a_type env sigma j
+
 let inh_tosort_force loc env evd j =
   try
-    let t,p = lookup_path_to_sort_from env evd (EConstr.of_constr j.uj_type) in
+    let t,p = lookup_path_to_sort_from env evd j.uj_type in
     let evd,j1 = apply_coercion env evd p j t in
+    let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in
     let j2 = on_judgment_type (whd_evar evd) j1 in
-      (evd,type_judgment env j2)
+      (evd,type_judgment env evd j2)
   with Not_found | NoCoercion ->
     error_not_a_type ~loc env evd j
 
 let inh_coerce_to_sort loc env evd j =
-  let typ = whd_all env evd (EConstr.of_constr j.uj_type) in
+  let typ = whd_all env evd j.uj_type in
     match EConstr.kind evd (EConstr.of_constr typ) with
     | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev ->
@@ -437,10 +443,10 @@ let inh_coerce_to_sort loc env evd j =
 let inh_coerce_to_base loc env evd j =
   if Flags.is_program_mode () then
     let evdref = ref evd in
-    let ct, typ' = mu env evdref (EConstr.of_constr j.uj_type) in
+    let ct, typ' = mu env evdref j.uj_type in
     let res =
-      { uj_val = EConstr.Unsafe.to_constr (app_coercion env evdref ct (EConstr.of_constr j.uj_val));
-	uj_type = EConstr.Unsafe.to_constr typ' }
+      { uj_val = (app_coercion env evdref ct j.uj_val);
+	uj_type = typ' }
     in !evdref, res
   else (evd, j)
 
@@ -463,8 +469,8 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
 	  | Some v ->
 	    let evd,j =
 	      apply_coercion env evd p
-		{uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr t} t2 in
-	      evd, Some (EConstr.of_constr j.uj_val), (EConstr.of_constr j.uj_type)
+		{uj_val = v; uj_type = t} t2 in
+	      evd, Some j.uj_val, j.uj_type
 	  | None -> evd, None, t
       with Not_found -> raise NoCoercion
     in
@@ -510,27 +516,27 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
 let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
   let (evd', val') =
     try
-      inh_conv_coerce_to_fail loc env evd rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
     with NoCoercionNoUnifier (best_failed_evd,e) ->
       try
 	if Flags.is_program_mode () then
-	  coerce_itf loc env evd (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+	  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 	else raise NoSubtacCoercion
       with
       | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
-	  error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+	  error_actual_type ~loc env best_failed_evd cj t e
       | NoSubtacCoercion ->
 	let evd' = saturate_evd env evd in
       	  try
 	    if evd' == evd then 
-	      error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+	      error_actual_type ~loc env best_failed_evd cj t e
 	    else 
-      	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+      	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
 	  with NoCoercionNoUnifier (_evd,_error) ->
-	    error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+	    error_actual_type ~loc env best_failed_evd cj t e
   in
   let val' = match val' with Some v -> v | None -> assert(false) in
-    (evd',{ uj_val = EConstr.Unsafe.to_constr val'; uj_type = EConstr.Unsafe.to_constr t })
+    (evd',{ uj_val = val'; uj_type = t })
 
 let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false
 let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 62d4fb004..bc63d092d 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -10,6 +10,7 @@ open Evd
 open Names
 open Term
 open Environ
+open EConstr
 open Glob_term
 
 (** {6 Coercions. } *)
@@ -36,7 +37,7 @@ val inh_coerce_to_base : Loc.t ->
 
 (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
 val inh_coerce_to_prod : Loc.t ->
-  env -> evar_map -> EConstr.types -> evar_map * EConstr.types
+  env -> evar_map -> types -> evar_map * types
 
 (** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an 
     object of type [t]; i.e. it inserts a coercion into [j], if needed, in such
@@ -44,16 +45,16 @@ val inh_coerce_to_prod : Loc.t ->
     applicable. resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
 val inh_conv_coerce_to : bool -> Loc.t ->
-  env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment
+  env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 val inh_conv_coerce_rigid_to : bool -> Loc.t ->
-  env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment
+  env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
     is coercible to an object of type [t'] adding evar constraints if needed;
     it fails if no coercion exists *)
 val inh_conv_coerces_to : Loc.t ->
-  env -> evar_map -> EConstr.types -> EConstr.types -> evar_map
+  env -> evar_map -> types -> types -> evar_map
 
 (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
     pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3b420347b..639d6260e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1266,8 +1266,8 @@ let solve_unconstrained_impossible_cases env evd =
       let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in
       let ty = j_type j in
       let conv_algo = evar_conv_x full_transparent_state in
-      let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) conv_algo in
-	Evd.define evk ty evd' 
+      let evd' = check_evar_instance evd' evk ty conv_algo in
+	Evd.define evk (EConstr.Unsafe.to_constr ty) evd' 
     | _ -> evd') evd evd
 
 let consider_remaining_unif_problems env
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 14b25ab36..673554005 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -31,11 +31,13 @@ type position_reporting = (position * int) * EConstr.t
 
 type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
 
+type type_error = (EConstr.constr, EConstr.types) ptype_error
+
 type pretype_error =
   (* Old Case *)
-  | CantFindCaseType of constr
+  | CantFindCaseType of EConstr.constr
   (* Type inference unification *)
-  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+  | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
   (* Tactic unification *)
   | UnifOccurCheck of existential_key * EConstr.constr
   | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
@@ -50,7 +52,7 @@ type pretype_error =
   | NonLinearUnification of Name.t * EConstr.constr
   (* Pretyping *)
   | VarNotFound of Id.t
-  | UnexpectedType of constr * constr
+  | UnexpectedType of EConstr.constr * EConstr.constr
   | NotProduct of EConstr.constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
@@ -75,14 +77,19 @@ let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason =
   raise_pretype_error ?loc
     (env, sigma, ActualTypeNotCoercible (j, expty, reason))
 
+let error_actual_type_core ?loc env sigma {uj_val=c;uj_type=actty} expty =
+  let j = {uj_val=c;uj_type=actty} in
+  raise_type_error ?loc
+    (env, sigma, ActualType (j, expty))
+
 let error_cant_apply_not_functional ?loc env sigma rator randl =
   raise_type_error ?loc
-    (env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
+    (env, sigma, CantApplyNonFunctional (rator, randl))
 
 let error_cant_apply_bad_type ?loc env sigma (n,c,t) rator randl =
   raise_type_error ?loc
     (env, sigma,
-       CantApplyBadType ((n,c,t), rator, Array.of_list randl))
+       CantApplyBadType ((n,c,t), rator, randl))
 
 let error_ill_formed_branch ?loc env sigma c i actty expty =
   raise_type_error
@@ -98,9 +105,16 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys =
   raise_type_error ?loc
     (env, sigma, IllTypedRecBody (i, na, jl, tys))
 
+let error_elim_arity ?loc env sigma pi s c j a =
+  raise_type_error ?loc
+    (env, sigma, ElimArity (pi, s, c, j, a))
+
 let error_not_a_type ?loc env sigma j =
   raise_type_error ?loc (env, sigma, NotAType j)
 
+let error_assumption ?loc env sigma j =
+  raise_type_error ?loc (env, sigma, BadAssumption j)
+
 (*s Implicit arguments synthesis errors. It is hard to find
     a precise location. *)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 2e707a0ff..0ebe4817c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -32,11 +32,13 @@ type position_reporting = (position * int) * EConstr.t
 
 type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
 
+type type_error = (EConstr.constr, EConstr.types) ptype_error
+
 type pretype_error =
   (** Old Case *)
-  | CantFindCaseType of constr
+  | CantFindCaseType of EConstr.constr
   (** Type inference unification *)
-  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+  | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
   (** Tactic Unification *)
   | UnifOccurCheck of existential_key * EConstr.constr
   | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
@@ -51,7 +53,7 @@ type pretype_error =
   | NonLinearUnification of Name.t * EConstr.constr
   (** Pretyping *)
   | VarNotFound of Id.t
-  | UnexpectedType of constr * constr
+  | UnexpectedType of EConstr.constr * EConstr.constr
   | NotProduct of EConstr.constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
@@ -65,34 +67,45 @@ val precatchable_exception : exn -> bool
 
 (** Raising errors *)
 val error_actual_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr ->
       unification_error -> 'b
 
+val error_actual_type_core :
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b
+
 val error_cant_apply_not_functional :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      unsafe_judgment -> unsafe_judgment list -> 'b
+      EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
 
 val error_cant_apply_bad_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr ->
-      unsafe_judgment -> unsafe_judgment list -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> int * EConstr.constr * EConstr.constr ->
+      EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
 
 val error_case_not_inductive :
-  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
 
 val error_ill_formed_branch :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      constr -> pconstructor -> constr -> constr -> 'b
+      EConstr.constr -> pconstructor -> EConstr.constr -> EConstr.constr -> 'b
 
 val error_number_branches :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      unsafe_judgment -> int -> 'b
+      EConstr.unsafe_judgment -> int -> 'b
 
 val error_ill_typed_rec_body :
   ?loc:Loc.t -> env -> Evd.evar_map ->
-      int -> Name.t array -> unsafe_judgment array -> types array -> 'b
+      int -> Name.t array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b
+
+val error_elim_arity :
+  ?loc:Loc.t -> env -> Evd.evar_map ->
+      pinductive -> sorts_family list -> EConstr.constr ->
+      EConstr.unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b
 
 val error_not_a_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
+
+val error_assumption :
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
 
 val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b
 
@@ -124,12 +137,12 @@ val error_non_linear_unification : env -> Evd.evar_map ->
 (** {6 Ml Case errors } *)
 
 val error_cant_find_case_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
 
 (** {6 Pretyping errors } *)
 
 val error_unexpected_type :
-  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b
 
 val error_not_product :
   ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cac31a1c5..49a0bccee 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -34,6 +34,7 @@ open Reductionops
 open Environ
 open Type_errors
 open Typeops
+open Typing
 open Globnames
 open Nameops
 open Evarutil
@@ -124,7 +125,7 @@ let e_new_evar env evdref ?src ?naming typ =
   let sigma = Sigma.Unsafe.of_evar_map !evdref in
   let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in
   evdref := Sigma.to_evar_map sigma;
-  e
+  EConstr.of_constr e
 
 let push_rec_types (lna,typarray,_) env =
   let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in
@@ -425,21 +426,19 @@ let invert_ltac_bound_name lvar env id0 id =
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
-  try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
+  try EConstr.of_constr (Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c)
   with Retyping.RetypeError _ ->
     user_err 
       (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++
        str " in the current environment.")
 
-let j_val j = EConstr.of_constr (j_val j)
-
 let pretype_id pretype k0 loc env evdref lvar id =
   let sigma = !evdref in
   (* Look for the binder of [id] *)
   try
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
     let typ = EConstr.of_constr typ in
-      { uj_val  = EConstr.Unsafe.to_constr (mkRel n); uj_type = EConstr.Unsafe.to_constr (lift n typ) }
+      { 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 *)
@@ -447,7 +446,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
       let (ids,c) = Id.Map.find id lvar.ltac_constrs in
       let subst = List.map (invert_ltac_bound_name lvar env id) ids in
       let c = substl subst (EConstr.of_constr c) in
-	{ uj_val = EConstr.Unsafe.to_constr c; uj_type = protected_get_type_of env sigma c }
+	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found -> try
        let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in
        let lvar = {
@@ -472,7 +471,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
       end;
       (* Check if [id] is a section or goal variable *)
       try
-	  { uj_val  = Constr.mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) }
+	  { uj_val  = mkVar id; uj_type = EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) }
       with Not_found ->
 	  (* [id] not found, standard error message *)
 	  error_var_not_found ~loc id
@@ -511,9 +510,6 @@ let pretype_global loc rigid env evd gr us =
   let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
   (sigma, EConstr.of_constr c)
 
-let make_judge c t =
-  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t)
-
 let pretype_ref loc evdref env ref us =
   match ref with
   | VarRef id ->
@@ -527,14 +523,14 @@ 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.unsafe_type_of env.ExtraEnv.env evd c in
+    let ty = unsafe_type_of env.ExtraEnv.env evd c in
     let ty = EConstr.of_constr ty in
       make_judge c ty
 
 let judge_of_Type loc evd s =
   let evd, s = interp_universe ~loc evd s in
   let judge = 
-    { uj_val = Constr.mkSort (Type s); uj_type = Constr.mkSort (Type (Univ.super s)) }
+    { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
   in
     evd, judge
 
@@ -550,7 +546,7 @@ let new_type_evar env evdref loc =
       univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
   in
   evdref := Sigma.to_evar_map sigma;
-  e
+  EConstr.of_constr e
 
 let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 
@@ -591,25 +587,25 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let env = ltac_interp_name_env k0 lvar env in
     let ty =
       match tycon with
-      | Some ty -> EConstr.Unsafe.to_constr ty
+      | Some ty -> ty
       | None -> new_type_evar env evdref loc in
     let k = Evar_kinds.MatchingVar (someta,n) in
-      { uj_val = e_new_evar env evdref ~src:(loc,k) (EConstr.of_constr ty); uj_type = ty }
+      { 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 -> EConstr.Unsafe.to_constr ty
+        | Some ty -> ty
         | None ->
           new_type_evar env evdref loc in
-        { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming (EConstr.of_constr ty); uj_type = ty }
+        { 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 -> EConstr.Unsafe.to_constr ty
+        | Some ty -> ty
         | None ->
           new_type_evar env evdref loc in
       let ist = lvar.ltac_genargs in
@@ -622,14 +618,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     [] -> ctxt
       | (na,bk,None,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
-	let dcl = LocalAssum (na, ty'.utj_val) in
-        let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in
+	let dcl = local_assum (na, ty'.utj_val) in
+        let dcl' = local_assum (ltac_interp_name lvar na,ty'.utj_val) in
 	  type_bl (push_rel dcl env) (Context.Rel.add 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 (EConstr.of_constr ty'.utj_val)) env evdref lvar bd in
-        let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
-        let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
+        let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
+        let dcl = local_def (na, bd'.uj_val, ty'.utj_val) in
+        let dcl' = local_def (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
 	  type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in
     let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
     let larj =
@@ -637,8 +633,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         (fun e ar ->
           pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
         ctxtv lar in
-    let lara = Array.map (fun a -> EConstr.of_constr a.utj_val) larj in
-    let ftys = Array.map2 (fun e a -> EConstr.it_mkProd_or_LetIn a e) ctxtv lara in
+    let lara = Array.map (fun a -> a.utj_val) larj in
+    let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
     let nbfix = Array.length lar in
     let names = Array.map (fun id -> Name id) names in
     let _ = 
@@ -662,8 +658,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
               (lift nbfix ftys.(i)) in
           let nenv = push_rel_context ctxt newenv in
           let j = pretype (mk_tycon ty) nenv evdref lvar def in
-	    { uj_val = Termops.it_mkLambda_or_LetIn j.uj_val ctxt;
-	      uj_type = Termops.it_mkProd_or_LetIn j.uj_type ctxt })
+	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
       Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj;
       let nf c = nf_evar !evdref c in
@@ -714,11 +710,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	(* Bidirectional typechecking hint: 
 	   parameters of a constructor are completely determined
 	   by a typing constraint *)
-      if Flags.is_program_mode () && length > 0 && isConstruct !evdref (EConstr.of_constr fj.uj_val) then
+      if Flags.is_program_mode () && length > 0 && isConstruct !evdref fj.uj_val then
 	match tycon with
 	| None -> []
 	| Some ty ->
-	  let ((ind, i), u) = destConstruct !evdref (EConstr.of_constr fj.uj_val) in
+	  let ((ind, i), u) = destConstruct !evdref fj.uj_val in
 	  let npars = inductive_nparams ind in
 	    if Int.equal npars 0 then []
 	    else
@@ -731,7 +727,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       else []
     in
     let app_f = 
-      match EConstr.kind !evdref (EConstr.of_constr fj.uj_val) with
+      match EConstr.kind !evdref fj.uj_val with
       | Const (p, u) when Environ.is_projection p env.ExtraEnv.env ->
 	let p = Projection.make p false in
 	let pb = Environ.lookup_projection p env.ExtraEnv.env in
@@ -746,7 +742,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       | c::rest ->
 	let argloc = loc_of_glob_constr c in
 	let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in
-        let resty = whd_all env.ExtraEnv.env !evdref (EConstr.of_constr resj.uj_type) in
+        let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in
         let resty = EConstr.of_constr resty in
       	  match EConstr.kind !evdref resty with
 	  | Prod (na,c1,c2) ->
@@ -761,18 +757,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		else [], j_val hj
 	    in
 	    let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
-	    let j = { uj_val = EConstr.Unsafe.to_constr value; uj_type = EConstr.Unsafe.to_constr typ } in
+	    let j = { uj_val = value; uj_type = typ } in
 	      apply_rec env (n+1) j candargs rest
 		
 	  | _ ->
 	    let hj = pretype empty_tycon env evdref lvar c in
 	      error_cant_apply_not_functional
                 ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref
-                resj [hj]
+                resj [|hj|]
     in
     let resj = apply_rec env 1 fj candargs args in
     let resj =
-      match EConstr.kind !evdref (EConstr.of_constr resj.uj_val) with
+      match EConstr.kind !evdref resj.uj_val with
       | App (f,args) ->
           if is_template_polymorphic env.ExtraEnv.env !evdref f then
 	    (* Special case for inductive type applications that must be 
@@ -804,7 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     (* 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 var = LocalAssum (name, j.utj_val) in
+    let var = local_assum (name, 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.ExtraEnv.env (orelse_name name name') j j' in
@@ -818,9 +814,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let j' = match name with
       | Anonymous ->
         let j = pretype_type empty_valcon env evdref lvar c2 in
-          { j with utj_val = EConstr.Unsafe.to_constr (lift 1 (EConstr.of_constr j.utj_val)) }
+          { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
-        let var = LocalAssum (name, j.utj_val) in
+        let var = local_assum (name, j.utj_val) in
         let env' = push_rel var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
@@ -839,27 +835,27 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       match c1 with
       | GCast (loc, c, CastConv t) ->
 	let tj = pretype_type empty_valcon env evdref lvar t in
-	  pretype (mk_tycon (EConstr.of_constr tj.utj_val)) env evdref lvar c
+	  pretype (mk_tycon tj.utj_val) env evdref lvar c
       | _ -> pretype empty_tycon env evdref lvar c1
     in
     let t = evd_comb1 (Evarsolve.refresh_universes
       ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
-      evdref (EConstr.of_constr j.uj_type) in
+      evdref j.uj_type in
+    let t = EConstr.of_constr t in
     (* 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 var = LocalDef (name, j.uj_val, t) in
-    let t = EConstr.of_constr t in
+    let var = local_def (name, 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 = EConstr.Unsafe.to_constr (mkLetIn (name, EConstr.of_constr j.uj_val, t, EConstr.of_constr j'.uj_val)) ;
-	uj_type = EConstr.Unsafe.to_constr (subst1 (EConstr.of_constr j.uj_val) (EConstr.of_constr j'.uj_type)) }
+      { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
+	uj_type = subst1 j.uj_val j'.uj_type }
 
   | GLetTuple (loc,nal,(na,po),c,d) ->
     let cj = pretype empty_tycon env evdref lvar c in
     let (IndType (indf,realargs)) =
-      try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type)
+      try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
 	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj
@@ -883,7 +879,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | na :: names, (LocalAssum (_,t) :: l) ->
             let t = EConstr.of_constr t in
 	    let proj = Projection.make ps.(cs.cs_nargs - k) true in
-	    local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, EConstr.of_constr cj.uj_val)), t)
+	    local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t)
 	    :: aux (n+1) (k + 1) names l
 	  | na :: names, (decl :: l) ->
 	    set_name na decl :: aux (n+1) k names l
@@ -897,7 +893,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         let fsign = List.map2 set_name nal fsign in
 	let f = it_mkLambda_or_LetIn f fsign in
 	let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in
-	  mkCase (ci, p, EConstr.of_constr cj.uj_val,[|f|]) 
+	  mkCase (ci, p, cj.uj_val,[|f|]) 
       else it_mkLambda_or_LetIn f fsign
     in
     let env_f = push_rel_context fsign env in
@@ -914,7 +910,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | Some p ->
 	    let env_p = push_rel_context psign env in
 	    let pj = pretype_type empty_valcon env_p evdref lvar p in
-	    let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in
+	    let ccl = nf_evar !evdref pj.utj_val in
 	    let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *)
 	    let p = it_mkLambda_or_LetIn ccl psign in
 	    let inst =
@@ -922,18 +918,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	      @[EConstr.of_constr (build_dependent_constructor cs)] in
 	    let lp = lift cs.cs_nargs p in
 	    let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in
-	    let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in
+	    let fty = EConstr.of_constr fty in
+	    let fj = pretype (mk_tycon fty) env_f evdref lvar d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p;
-		obj ind p cj.uj_val (EConstr.of_constr fj.uj_val)
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+		obj ind p cj.uj_val fj.uj_val
 	    in
-	      { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr (substl (realargs@[EConstr.of_constr cj.uj_val]) ccl) }
+	      { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) }
 
 	  | None ->
 	    let tycon = lift_tycon cs.cs_nargs tycon in
 	    let fj = pretype tycon env_f evdref lvar d in
-	    let ccl = nf_evar !evdref (EConstr.of_constr fj.uj_type) in
+	    let ccl = nf_evar !evdref fj.uj_type in
 	    let ccl =
 	      if noccur_between !evdref 1 cs.cs_nargs ccl then
 		lift (- cs.cs_nargs) ccl
@@ -944,14 +941,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p;
-		obj ind p cj.uj_val (EConstr.of_constr fj.uj_val)
-	    in { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr ccl })
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+		obj ind p cj.uj_val fj.uj_val
+	    in { uj_val = v; uj_type = ccl })
 
   | GIf (loc,c,(na,po),b1,b2) ->
     let cj = pretype empty_tycon env evdref lvar c in
     let (IndType (indf,realargs)) =
-      try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type)
+      try find_rectype env.ExtraEnv.env !evdref cj.uj_type
       with Not_found ->
 	let cloc = loc_of_glob_constr c in
 	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in
@@ -973,16 +970,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	| Some p ->
 	  let env_p = push_rel_context psign env in
 	  let pj = pretype_type empty_valcon env_p evdref lvar p in
-	  let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in
+	  let ccl = nf_evar !evdref pj.utj_val in
 	  let pred = it_mkLambda_or_LetIn ccl psign in
-	  let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[EConstr.of_constr cj.uj_val]))) in
+	  let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[cj.uj_val]))) in
 	    pred, typ
 	| None ->
 	  let p = match tycon with
 	    | Some ty -> ty
 	    | None ->
               let env = ltac_interp_name_env k0 lvar env in
-              EConstr.of_constr (new_type_evar env evdref loc)
+              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
@@ -991,6 +988,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let n = Context.Rel.length cs.cs_args in
 	let pi = lift n pred in (* liftn n 2 pred ? *)
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
+	let pi = EConstr.of_constr pi in
 	let csgn =
 	  if not !allow_anonymous_refs then
 	    List.map (set_name Anonymous) cs.cs_args
@@ -1000,18 +998,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		     cs.cs_args
 	in
 	let env_c = push_rel_context csgn env in
-	let bj = pretype (mk_tycon (EConstr.of_constr pi)) env_c evdref lvar b in
-	  it_mkLambda_or_LetIn (EConstr.of_constr bj.uj_val) cs.cs_args in
+	let bj = pretype (mk_tycon pi) env_c evdref lvar b in
+	  it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
       let b1 = f cstrs.(0) b1 in
       let b2 = f cstrs.(1) b2 in
       let v =
 	let ind,_ = dest_ind_family indf in
 	let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
 	let pred = nf_evar !evdref pred in
-	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) pred;
-	  mkCase (ci, pred, EConstr.of_constr cj.uj_val, [|b1;b2|])
+	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
+	  mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
-      let cj = { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr p } in
+      let cj = { uj_val = v; uj_type = p } in
       inh_conv_coerce_to_tycon loc env evdref cj tycon
 
   | GCases (loc,sty,po,tml,eqns) ->
@@ -1030,36 +1028,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let tj = pretype_type empty_valcon env evdref lvar t in
         let tval = evd_comb1 (Evarsolve.refresh_universes
                              ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
-                          evdref (EConstr.of_constr tj.utj_val) in
+                          evdref tj.utj_val in
         let tval = EConstr.of_constr tval in
 	let tval = nf_evar !evdref tval in
 	let cj, tval = match k with
 	  | VMcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
-	    let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in
+	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
 	      if not (occur_existential !evdref cty || occur_existential !evdref tval) then
 		let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
 		if b then (evdref := evd; cj, tval)
 		else
-		  error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) 
+		  error_actual_type ~loc env.ExtraEnv.env !evdref cj tval 
                       (ConversionFailed (env.ExtraEnv.env,cty,tval))
 	      else user_err ~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 (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in
+	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
             begin
 	      let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
 	      if b then (evdref := evd; cj, tval)
 	      else
-                error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval)
+                error_actual_type ~loc env.ExtraEnv.env !evdref cj tval
                   (ConversionFailed (env.ExtraEnv.env,cty,tval))
             end
 	  | _ -> 
  	    pretype (mk_tycon tval) env evdref lvar c, tval
 	in
-	let v = mkCast (EConstr.of_constr cj.uj_val, k, tval) in
-	  { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr tval }
+	let v = mkCast (cj.uj_val, k, tval) in
+	  { uj_val = v; uj_type = tval }
     in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
 and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
@@ -1070,7 +1068,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
       try
         let c = List.assoc id update in
         let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
-        EConstr.of_constr c.uj_val, List.remove_assoc id update
+        c.uj_val, List.remove_assoc id update
       with Not_found ->
       try
         let (n,_,t') = lookup_rel_id id (rel_context env) in
@@ -1103,13 +1101,14 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
            let s =
 	     let sigma =  !evdref in
 	     let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
-	       match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t))) with
+	     let t = EConstr.of_constr t in
+	       match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma t)) with
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
 		   evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
                | _ -> anomaly (Pp.str "Found a type constraint which is not a type")
            in
-	     { utj_val = EConstr.Unsafe.to_constr v;
+	     { utj_val = v;
 	       utj_type = s }
        | None ->
            let env = ltac_interp_name_env k0 lvar env in
@@ -1123,10 +1122,10 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	match valcon with
 	| None -> tj
 	| Some v ->
-	    if e_cumul env.ExtraEnv.env evdref v (EConstr.of_constr tj.utj_val) then tj
+	    if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
 	    else
 	      error_unexpected_type
-                ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val (EConstr.Unsafe.to_constr v)
+                ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let env = make_env env in
@@ -1140,7 +1139,7 @@ let ise_pretype_gen flags env sigma lvar kind c =
     | IsType ->
 	(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
   in
-  process_inference_flags flags env.ExtraEnv.env sigma (!evdref,EConstr.of_constr c')
+  process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c')
 
 let default_inference_flags fail = {
   use_typeclasses = true;
@@ -1167,9 +1166,9 @@ let empty_lvar : ltac_var_map = {
 }
 
 let on_judgment sigma f j =
-  let c = mkCast(EConstr.of_constr j.uj_val,DEFAULTcast, EConstr.of_constr j.uj_type) in
+  let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in
   let (c,_,t) = destCast sigma (f c) in
-  {uj_val = EConstr.Unsafe.to_constr c; uj_type = EConstr.Unsafe.to_constr t}
+  {uj_val = c; uj_type = t}
 
 let understand_judgment env sigma c =
   let env = make_env env in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 603b9f9ea..2f3ce3afa 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -110,11 +110,11 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
 (** Idem but returns the judgment of the understood term *)
 
 val understand_judgment : env -> evar_map -> 
-  glob_constr -> unsafe_judgment Evd.in_evar_universe_context
+  glob_constr -> EConstr.unsafe_judgment Evd.in_evar_universe_context
 
 (** Idem but do not fail on unresolved evars (type cl*)
 val understand_judgment_tcc : env -> evar_map ref ->
-  glob_constr -> unsafe_judgment
+  glob_constr -> EConstr.unsafe_judgment
 
 val type_uconstr :
   ?flags:inference_flags ->
@@ -145,11 +145,11 @@ val check_evars : env -> evar_map -> evar_map -> EConstr.constr -> unit
 (** Internal of Pretyping... *)
 val pretype :
   int -> bool -> type_constraint -> env -> evar_map ref ->
-  ltac_var_map -> glob_constr -> unsafe_judgment
+  ltac_var_map -> glob_constr -> EConstr.unsafe_judgment
 
 val pretype_type :
   int -> bool -> val_constraint -> env -> evar_map ref ->
-  ltac_var_map -> glob_constr -> unsafe_type_judgment
+  ltac_var_map -> glob_constr -> EConstr.unsafe_type_judgment
 
 val ise_pretype_gen :
   inference_flags -> env -> evar_map ->
@@ -163,5 +163,5 @@ val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
 val interp_elimination_sort : glob_sort -> sorts_family
 
 val genarg_interp_hook :
-  (types -> env -> evar_map -> unbound_ltac_var_map ->
-    Genarg.glob_generic_argument -> constr * evar_map) Hook.t
+  (EConstr.types -> env -> evar_map -> unbound_ltac_var_map ->
+    Genarg.glob_generic_argument -> EConstr.constr * evar_map) Hook.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 2efb02417..a7ccf98a6 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -244,7 +244,7 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
     if lax then EConstr.Unsafe.to_constr (f env c) else EConstr.Unsafe.to_constr (anomaly_on_error (f env) c)
 
 (* Makes an unsafe judgment from a constr *)
-let get_judgment_of env evc c = { uj_val = EConstr.Unsafe.to_constr c; uj_type = get_type_of env evc c }
+let get_judgment_of env evc c = { uj_val = c; uj_type = EConstr.of_constr (get_type_of env evc c) }
 
 (* Returns sorts of a context *)
 let sorts_of_context env evc ctxt =
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 08f750287..c84403890 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -35,7 +35,7 @@ val get_sort_family_of :
   ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts_family
 
 (** Makes an unsafe judgment from a constr *)
-val get_judgment_of : env -> evar_map -> EConstr.constr -> unsafe_judgment
+val get_judgment_of : env -> evar_map -> EConstr.constr -> EConstr.unsafe_judgment
 
 val type_of_global_reference_knowing_parameters : env -> evar_map -> EConstr.constr ->
   EConstr.constr array -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c948f9b9a..17adea5f2 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -6,20 +6,31 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
+
 open Pp
 open CErrors
 open Util
 open Term
+open EConstr
 open Vars
 open Environ
 open Reductionops
-open Type_errors
 open Inductive
 open Inductiveops
 open Typeops
 open Arguments_renaming
+open Pretype_errors
 open Context.Rel.Declaration
 
+let local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
 let push_rec_types pfix env =
   let (i, c, t) = pfix in
   let inj c = EConstr.Unsafe.to_constr c in
@@ -31,57 +42,57 @@ let meta_type evd mv =
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
   meta_instance evd ty
 
-let constant_type_knowing_parameters env cst jl =
-  let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+let constant_type_knowing_parameters env sigma cst jl =
+  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
   EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
 
-let inductive_type_knowing_parameters env (ind,u) jl =
+let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let mspec = lookup_mind_specif env ind in
-  let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
+  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
-  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
+  match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref j.uj_type)) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
         let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
         evdref := evd; { utj_val = j.uj_val; utj_type = s }
-    | _ -> error_not_type env j
+    | _ -> error_not_a_type env !evdref j
 
 let e_assumption_of_judgment env evdref j =
-  try EConstr.of_constr (e_type_judgment env evdref j).utj_val
-  with TypeError _ ->
-    error_assumption env j
+  try (e_type_judgment env evdref j).utj_val
+  with Type_errors.TypeError _ | PretypeError _ ->
+    error_assumption env !evdref j
 
 let e_judge_of_apply env evdref funj argjv =
   let open EConstr in
   let rec apply_rec n typ = function
   | [] ->
-      { uj_val  = Constr.mkApp (j_val funj, Array.map j_val argjv);
-        uj_type = EConstr.Unsafe.to_constr typ }
+      { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
+        uj_type = typ }
   | hj::restjl ->
       match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
       | Prod (_,c1,c2) ->
-	 if Evarconv.e_cumul env evdref (EConstr.of_constr hj.uj_type) c1 then
-	   apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
+	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
+	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
 	 else
-	   error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv
+	   error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv
       | Evar ev ->
 	  let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
           evdref := evd';
           let (_,_,c2) = destProd evd' t in
-	  apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl
+	  apply_rec (n+1) (subst1 hj.uj_val c2) restjl
       | _ ->
-	  error_cant_apply_not_functional env funj argjv
+	  error_cant_apply_not_functional env !evdref funj argjv
   in
-  apply_rec 1 (EConstr.of_constr funj.uj_type) (Array.to_list argjv)
+  apply_rec 1 funj.uj_type (Array.to_list argjv)
 
 let e_check_branch_types env evdref (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
-    error_number_branches env cj (Array.length explft);
+    error_number_branches env !evdref cj (Array.length explft);
   for i = 0 to Array.length explft - 1 do
-    if not (Evarconv.e_cumul env evdref (EConstr.of_constr lfj.(i).uj_type) (EConstr.of_constr explft.(i))) then
-      error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
+    if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
+      error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i)
   done
 
 let max_sort l =
@@ -92,13 +103,13 @@ let e_is_correct_arity env evdref c pj ind specif params =
   let open EConstr in
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
-  let error () = error_elim_arity env ind allowed_sorts c pj None in
+  let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in
   let rec srec env pt ar =
     let pt' = EConstr.of_constr (whd_all env !evdref pt) in
     match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
         if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
-        srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar'
+        srec (push_rel (local_assum (na1,a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
@@ -106,27 +117,43 @@ let e_is_correct_arity env evdref c pj ind specif params =
         let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
         evdref := Evd.define ev (Constr.mkSort s) evd
     | _, (LocalDef _ as d)::ar' ->
-        srec (push_rel d env) (Vars.lift 1 pt') ar'
+        srec (push_rel d env) (lift 1 pt') ar'
     | _ ->
         error ()
   in
-  srec env (EConstr.of_constr pj.uj_type) (List.rev arsign)
+  srec env pj.uj_type (List.rev arsign)
+
+let lambda_applist_assum sigma n c l =
+  let open EConstr in
+  let rec app n subst t l =
+    if Int.equal n 0 then
+      if l == [] then substl subst t
+      else anomaly (Pp.str "Not enough arguments")
+    else match EConstr.kind sigma t, l with
+    | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+    | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _ -> anomaly (Pp.str "Not enough lambda/let's") in
+  app n [] c l
 
 let e_type_case_branches env evdref (ind,largs) pj c =
   let specif = lookup_mind_specif env (fst ind) in
   let nparams = inductive_params specif in
   let (params,realargs) = List.chop nparams largs in
   let p = pj.uj_val in
+  let realargs = List.map EConstr.of_constr realargs in
   let () = e_is_correct_arity env evdref c pj ind specif params in
-  let lc = build_branches_type ind specif params p in
+  let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
+  let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
-  let ty = whd_betaiota !evdref (EConstr.of_constr (lambda_applist_assum (n+1) p (realargs@[c]))) in
+  let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
+  let ty = EConstr.of_constr ty in
   (lc, ty)
 
 let e_judge_of_case env evdref ci pj cj lfj =
+  let open EConstr in
   let indspec =
-    try find_mrectype env !evdref (EConstr.of_constr cj.uj_type)
-    with Not_found -> error_case_not_inductive env cj in
+    try find_mrectype env !evdref cj.uj_type
+    with Not_found -> error_case_not_inductive env !evdref cj in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
   e_check_branch_types env evdref (fst indspec) cj (lfj,bty);
@@ -138,27 +165,28 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
-        if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
-		  (Vars.lift lt lar.(i))) then
-          Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
-            i lna vdefj (Array.map EConstr.Unsafe.to_constr lar)
+        if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
+		  (lift lt lar.(i))) then
+          error_ill_typed_rec_body ~loc env !evdref
+            i lna vdefj lar
       done
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
+  let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
     let s = inductive_sort_family (snd specif) in
-    error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj
-      (Some(ksort,s,error_elim_explain ksort s))
+    error_elim_arity env sigma ind sorts c pj
+      (Some(ksort,s,Type_errors.error_elim_explain ksort s))
 
 let e_judge_of_cast env evdref cj k tj =
+  let open EConstr in
   let expected_type = tj.utj_val in
-  if not (Evarconv.e_cumul env evdref (EConstr.of_constr cj.uj_type) (EConstr.of_constr expected_type)) then
-    error_actual_type env cj expected_type;
+  if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+    error_actual_type_core env !evdref cj expected_type;
   { uj_val = mkCast (cj.uj_val, k, expected_type);
     uj_type = expected_type }
 
@@ -178,11 +206,56 @@ let check_cofix env sigma pcofix =
   let (idx, (ids, cs, ts)) = pcofix in
   check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
 
-let make_judge c ty =
-  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
-			  
 (* The typing machine with universes and existential variables. *)
 
+let judge_of_prop =
+  { uj_val = EConstr.mkProp;
+    uj_type = EConstr.mkSort type1_sort }
+
+let judge_of_set =
+  { uj_val = EConstr.mkSet;
+    uj_type = EConstr.mkSort type1_sort }
+
+let judge_of_prop_contents = function
+  | Null -> judge_of_prop
+  | Pos -> judge_of_set
+
+let judge_of_type u =
+  let uu = Univ.Universe.super u in
+    { uj_val = EConstr.mkType u;
+      uj_type = EConstr.mkType uu }
+
+let judge_of_relative env v =
+  Termops.on_judgment EConstr.of_constr (judge_of_relative env v)
+
+let judge_of_variable env id =
+  Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
+
+let judge_of_projection env sigma p cj =
+  let pb = lookup_projection p env in
+  let (ind,u), args =
+    try find_mrectype env sigma cj.uj_type
+    with Not_found -> error_case_not_inductive env sigma cj
+  in
+  let args = List.map EConstr.of_constr args in
+    let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in
+    let ty = substl (cj.uj_val :: List.rev args) ty in
+      {uj_val = EConstr.mkProj (p,cj.uj_val);
+       uj_type = ty}
+
+let judge_of_abstraction env name var j =
+  { uj_val = mkLambda (name, var.utj_val, j.uj_val);
+    uj_type = mkProd (name, var.utj_val, j.uj_type) }
+
+let judge_of_product env name t1 t2 =
+  let s = sort_of_product env t1.utj_type t2.utj_type in
+  { uj_val = mkProd (name, t1.utj_val, t2.utj_val);
+    uj_type = mkSort s }
+
+let judge_of_letin env name defj typj j =
+  { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
+    uj_type = subst1 defj.uj_val j.uj_type }
+
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
@@ -190,13 +263,13 @@ let rec execute env evdref cstr =
   let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
   match EConstr.kind !evdref cstr with
     | Meta n ->
-        { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n }
+        { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) }
 
     | Evar ev ->
 	let ty = EConstr.existential_type !evdref ev in
 	let jty = execute env evdref ty in
 	let jty = e_assumption_of_judgment env evdref jty in
-	{ uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty }
+	{ uj_val = cstr; uj_type = jty }
 
     | Rel n ->
 	judge_of_relative env n
@@ -239,7 +312,7 @@ let rec execute env evdref cstr =
 
     | Proj (p, c) -> 
         let cj = execute env evdref c in
-	  judge_of_projection env p (Evarutil.j_nf_evar !evdref cj)
+	  judge_of_projection env !evdref p cj
 
     | App (f,args) ->
         let jl = execute_array env evdref args in
@@ -248,13 +321,11 @@ let rec execute env evdref cstr =
 	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (inductive_type_knowing_parameters env ind
-		    (Evarutil.jv_nf_evar !evdref jl))
+		  (inductive_type_knowing_parameters env !evdref ind jl)
 	    | Const cst when Environ.template_polymorphic_pconstant cst env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
-		  (constant_type_knowing_parameters env cst
-		    (Evarutil.jv_nf_evar !evdref jl))
+		  (constant_type_knowing_parameters env !evdref cst jl)
 	    | _ ->
 		execute env evdref f
 	in
@@ -263,14 +334,14 @@ let rec execute env evdref cstr =
     | Lambda (name,c1,c2) ->
         let j = execute env evdref c1 in
 	let var = e_type_judgment env evdref j in
-	let env1 = push_rel (LocalAssum (name, var.utj_val)) env in
+	let env1 = push_rel (local_assum (name, var.utj_val)) env in
         let j' = execute env1 evdref c2 in
         judge_of_abstraction env1 name var j'
 
     | Prod (name,c1,c2) ->
         let j = execute env evdref c1 in
         let varj = e_type_judgment env evdref j in
-	let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in
+	let env1 = push_rel (local_assum (name, varj.utj_val)) env in
         let j' = execute env1 evdref c2 in
         let varj' = e_type_judgment env1 evdref j' in
 	judge_of_product env name varj varj'
@@ -280,7 +351,7 @@ let rec execute env evdref cstr =
         let j2 = execute env evdref c2 in
         let j2 = e_type_judgment env evdref j2 in
         let _ =  e_judge_of_cast env evdref j1 DEFAULTcast j2 in
-        let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in
+        let env1 = push_rel (local_def (name, j1.uj_val, j2.utj_val)) env in
         let j3 = execute env1 evdref c3 in
         judge_of_letin env name j1 j2 j3
 
@@ -295,7 +366,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let lara = Array.map (e_assumption_of_judgment env evdref) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
-  let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in
+  let vdefv = Array.map j_val vdefj in
   let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
   (names,lara,vdefv)
 
@@ -304,8 +375,8 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then
-    error_actual_type env j (EConstr.to_constr !evdref t)
+  if not (Evarconv.e_cumul env evdref j.uj_type t) then
+    error_actual_type_core env !evdref j t
 
 (* Type of a constr *)
 
@@ -313,7 +384,7 @@ let unsafe_type_of env evd c =
   let evdref = ref evd in
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-    j.uj_type
+    EConstr.Unsafe.to_constr j.uj_type
 
 (* Sort of a type *)
 
@@ -331,23 +402,23 @@ let type_of ?(refresh=false) env evd c =
   let j = execute env evdref c in
   (* side-effect on evdref *)
     if refresh then
-      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type)
-    else !evdref, j.uj_type
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type
+    else !evdref, EConstr.Unsafe.to_constr j.uj_type
 
 let e_type_of ?(refresh=false) env evdref c =
   let env = enrich_env env evdref in
   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 (EConstr.of_constr j.uj_type) in
+      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
+    else EConstr.Unsafe.to_constr j.uj_type
 
 let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
-  nf_evar !evdref c
+  nf_evar !evdref (EConstr.Unsafe.to_constr c)
 
 let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 3c1c4324d..1fb414906 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Term
 open Environ
 open Evd
@@ -43,4 +44,11 @@ val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> ECon
 (** Raise an error message if bodies have types not unifiable with the
     expected ones *)
 val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
-  Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit
+  Names.Name.t array -> EConstr.types array -> EConstr.unsafe_judgment array -> unit
+
+val judge_of_prop : EConstr.unsafe_judgment
+val judge_of_set : EConstr.unsafe_judgment
+val judge_of_abstraction : Environ.env -> Name.t ->
+  EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
+val judge_of_product : Environ.env -> Name.t ->
+  EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c5c19b49b..1b209fa77 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -120,6 +120,9 @@ let abstract_list_all env evd typ c l =
     | UserError _ ->
         error_cannot_find_well_typed_abstraction env evd p l None
     | Type_errors.TypeError (env',x) ->
+        (** FIXME: plug back the typing information *)
+        error_cannot_find_well_typed_abstraction env evd p l None
+    | Pretype_errors.PretypeError (env',evd,TypingError x) ->
         error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
   let typp = EConstr.of_constr typp in
   evd,(p,typp)
@@ -1255,15 +1258,12 @@ let is_mimick_head sigma ts f =
   | (Rel _|Construct _|Ind _) -> true
   | _ -> false
 
-let make_judge c t =
-  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t)
-
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
   let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in
   let evd' = Evarconv.consider_remaining_unif_problems env evd' in
   let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in
-    (evd',EConstr.of_constr j'.uj_val)
+    (evd',j'.uj_val)
 
 let w_coerce_to_type env evd c cty mvty =
   let evd,tycon = pose_all_metas_as_evars env evd mvty in