Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7

52 files changed, 395 insertions, 510 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index ae5e51db0..8f49130b7 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -738,15 +738,6 @@ and frreference =
 
 let reloc_flex r el = r
 
-(*
-let typed_map f t = f (body_of_type t), level_of_type t
-let typed_unmap f (t,s) = make_typed (f t) s
-*)
-(**)
-let typed_map f t = f (body_of_type t)
-let typed_unmap f t = make_typed_lazy (f t) (fun _ -> assert false)
-(**)
-
 let frterm_of v = v.term
 let is_val v = v.norm 
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 3b2ba2ece..883e20f3f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -18,7 +18,7 @@ type constant_value = lazy_constant_value ref
 type constant_body = {
   const_kind : path_kind;
   const_body : constant_value option;
-  const_type : typed_type;
+  const_type : types;
   const_hyps : named_context;
   const_constraints : constraints;
   mutable const_opaque : bool }
@@ -47,11 +47,11 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_nf_lc : typed_type array;
-  mind_nf_arity : typed_type;
+  mind_nf_lc : types array;
+  mind_nf_arity : types;
   (* lc and arity as given by user if not in nf; useful e.g. for Ensemble.v *)
-  mind_user_lc : typed_type array option;
-  mind_user_arity : typed_type option;
+  mind_user_lc : types array option;
+  mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3a85e7e05..3be72f3fd 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -22,7 +22,7 @@ type constant_value = lazy_constant_value ref
 type constant_body = {
   const_kind : path_kind;
   const_body : constant_value option;
-  const_type : typed_type;
+  const_type : types;
   const_hyps : named_context; (* New: younger hyp at top *)
   const_constraints : constraints;
   mutable const_opaque : bool }
@@ -56,10 +56,10 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_nf_lc : typed_type array; (* constrs and arity with pre-expanded ccl *)
-  mind_nf_arity : typed_type;
-  mind_user_lc : typed_type array option;
-  mind_user_arity : typed_type option;
+  mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
+  mind_nf_arity : types;
+  mind_user_lc : types array option;
+  mind_user_arity : types option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -76,8 +76,8 @@ type mutual_inductive_body = {
   mind_nparams : int }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
-val mind_user_lc : one_inductive_body -> typed_type array
-val mind_user_arity : one_inductive_body -> typed_type
+val mind_user_lc : one_inductive_body -> types array
+val mind_user_arity : one_inductive_body -> types
 val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body
 
 val mind_arities_context : mutual_inductive_body -> rel_declaration list
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 45ec56816..db7f78ba1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -111,13 +111,13 @@ let push_rel_context_to_named_context env =
        let na = if na = Anonymous then Name(id_of_string"_") else na in
        let id = next_name_away na avoid in
        ((mkVar id)::subst,id::avoid,
-	add_named_decl (id,option_app (substl subst) c,typed_app (substl subst) t)
+	add_named_decl (id,option_app (substl subst) c,type_app (substl subst) t)
 	  sign))
     env.env_context.env_rel_context ([],ids_of_named_context sign0,sign0)
   in subst, (named_context_app (fun _ -> sign) env)
 
 let push_rec_types (typarray,names,_) env =
-  let vect_lift_type = Array.mapi (fun i t -> outcast_type (lift i t)) in
+  let vect_lift_type = Array.mapi (fun i t -> lift i t) in
   let nlara = 
     List.combine (List.rev names) (Array.to_list (vect_lift_type typarray)) in
   List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara
@@ -264,18 +264,17 @@ let named_hd env a = function
   | Anonymous -> Name (id_of_string (hdchar env a)) 
   | x         -> x
 
-let prod_name   env (n,a,b) = mkProd (named_hd env a n, a, b)
-let lambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
+let named_hd_type env a = named_hd env (body_of_type a)
 
-let it_prod_name   env = List.fold_left (fun c (n,t) ->prod_name env (n,t,c)) 
-let it_lambda_name env = List.fold_left (fun c (n,t) ->lambda_name env (n,t,c))
+let prod_name   env (n,a,b) = mkProd (named_hd_type env a n, a, b)
+let lambda_name env (n,a,b) = mkLambda (named_hd_type env a n, a, b)
 
-let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
-let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
+let prod_create   env (a,b) = mkProd (named_hd_type env a Anonymous, a, b)
+let lambda_create env (a,b) =  mkLambda (named_hd_type env a Anonymous, a, b)
 
 let name_assumption env (na,c,t) =
   match c with
-    | None      -> (named_hd env (body_of_type t) na, None, t)
+    | None      -> (named_hd_type env t na, None, t)
     | Some body -> (named_hd env body na, c, t)
 
 let prod_assum_name env b d = mkProd_or_LetIn (name_assumption env d) b 
@@ -379,7 +378,7 @@ let import cenv env =
 
 type unsafe_judgment = { 
   uj_val : constr;
-  uj_type : typed_type }
+  uj_type : types }
 
 type unsafe_type_judgment = { 
   utj_val : constr;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 611987c90..ba75b8b77 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -30,16 +30,16 @@ val reset_context : env -> env
 
 (*s This concerns only local vars referred by names [named_context] *)
 val push_named_decl : named_declaration -> env -> env
-val push_named_assum : identifier * typed_type -> env -> env
-val push_named_def : identifier * constr * typed_type -> env -> env
+val push_named_assum : identifier * types -> env -> env
+val push_named_def : identifier * constr * types -> env -> env
 val change_hyps : (named_context -> named_context) -> env -> env
 val instantiate_named_context  : named_context -> constr list -> (identifier * constr) list
 val pop_named_decl : identifier -> env -> env
 
 (*s This concerns only local vars referred by indice [rel_context] *)
 val push_rel : rel_declaration -> env -> env
-val push_rel_assum : name * typed_type -> env -> env
-val push_rel_def : name * constr * typed_type -> env -> env
+val push_rel_assum : name * types -> env -> env
+val push_rel_def : name * constr * types -> env -> env
 val push_rels : rel_context -> env -> env
 val names_of_rel_context : env -> names_context
 
@@ -83,13 +83,13 @@ val new_meta : unit -> int
 
 (* Looks up in the context of local vars referred by names ([named_context]) *)
 (* raises [Not_found] if the identifier is not found *)
-val lookup_named_type : identifier -> env -> typed_type
+val lookup_named_type : identifier -> env -> types
 val lookup_named_value : identifier -> env -> constr option
-val lookup_named : identifier -> env -> constr option * typed_type
+val lookup_named : identifier -> env -> constr option * types
 
 (* Looks up in the context of local vars referred by indice ([rel_context]) *)
 (* raises [Not_found] if the index points out of the context *)
-val lookup_rel_type : int -> env -> name * typed_type
+val lookup_rel_type : int -> env -> name * types
 val lookup_rel_value : int -> env -> constr option
 
 (* Looks up in the context of global constant names *)
@@ -121,11 +121,8 @@ val named_hd : env -> constr -> name -> name
    first in [sign]; none of these functions substitute named
    variables in [c] by de Bruijn indices *)
 
-val lambda_name : env -> name * constr * constr -> constr
-val prod_name : env -> name * constr * constr -> constr
-
-val it_lambda_name : env -> constr -> (name * constr) list -> constr
-val it_prod_name : env -> constr -> (name * constr) list -> constr
+val lambda_name : env -> name * types * constr -> constr
+val prod_name : env -> name * types * constr -> constr
 
 val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
 val it_mkProd_or_LetIn_name : env -> constr -> rel_context -> constr
@@ -141,8 +138,8 @@ val it_mkNamedProd_or_LetIn : constr -> named_context -> constr
    from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
    name built from [t] *)
 
-val lambda_create : env -> constr * constr -> constr
-val prod_create : env -> constr * constr -> constr
+val lambda_create : env -> types * constr -> constr
+val prod_create : env -> types * constr -> constr
 
 val defined_constant : env -> constant -> bool
 val evaluable_constant : env -> constant -> bool
@@ -160,7 +157,7 @@ val import : compiled_env -> env -> env
 
 type unsafe_judgment = { 
   uj_val : constr;
-  uj_type : typed_type }
+  uj_type : types }
 
 type unsafe_type_judgment = { 
   utj_val : constr;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index fdfdf0052..acfea1109 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -180,7 +180,7 @@ let listrec_mconstr env ntypes nparams i indlc =
 	  assert (largs = []);
           if not (noccur_between n ntypes b) then
 	    raise (IllFormedInd (LocalNonPos n));
-	  check_pos (push_rel_assum (na, outcast_type b) env) (n+1) d
+	  check_pos (push_rel_assum (na, b) env) (n+1) d
       | IsRel k ->
           if k >= n && k<n+ntypes then begin
 	    check_correct_par env nparams ntypes n (k-n+1) largs;
@@ -246,7 +246,7 @@ let listrec_mconstr env ntypes nparams i indlc =
       (* The extra case *)
       | IsLambda (na,b,d) -> 
           if noccur_between n ntypes b
-          then check_weak_pos (push_rel_assum (na,outcast_type b) env) (n+1) d
+          then check_weak_pos (push_rel_assum (na,b) env) (n+1) d
           else raise (IllFormedInd (LocalNonPos n))
       (******************)
       | _ -> check_pos env n x
@@ -263,7 +263,7 @@ let listrec_mconstr env ntypes nparams i indlc =
         | IsProd (na,b,d) -> 
 	    assert (largs = []);
             let recarg = check_pos env n b in 
-	    check_constr_rec (push_rel_assum (na,outcast_type b) env)
+	    check_constr_rec (push_rel_assum (na, b) env)
 	      (recarg::lrec) (n+1) d
 
         (* LetIn's must be free of occurrence of the inductive types and
@@ -271,11 +271,11 @@ let listrec_mconstr env ntypes nparams i indlc =
         | IsLetIn (na,b,t,d) -> 
 	    assert (largs = []);
             if not (noccur_between n ntypes b & noccur_between n ntypes t) then
-	      check_constr_rec (push_rel_def (na,b,outcast_type b) env)
+	      check_constr_rec (push_rel_def (na,b, b) env)
 		lrec n (subst1 b d)
 	    else
               let recarg = check_pos env n b in 
-	      check_constr_rec (push_rel_def (na,b,outcast_type b) env)
+	      check_constr_rec (push_rel_def (na,b, b) env)
 		lrec (n+1) d 
 	| hd ->
 	    if check_head then
@@ -318,20 +318,13 @@ let cci_inductive env env_ar kind nparams finite inds cst =
     
     let nf_ar,user_ar =
       if isArity (body_of_type ar) then ar,None
-      else
-	(make_typed_lazy (prod_it (mkSort ar_sort) ar_sign)
-	   (fun _ -> level_of_type ar)),
-	Some ar in
+      else (prod_it (mkSort ar_sort) ar_sign, Some ar) in
     let kelim = allowed_sorts issmall isunit ar_sort in
     let lc_bodies = Array.map body_of_type lc in
 
     let splayed_lc = Array.map (splay_prod_assum env_ar Evd.empty) lc_bodies in
     let nf_lc =
-      array_map2
-	(fun (d,b) c ->
-	   make_typed_lazy 
-	     (it_mkProd_or_LetIn b d) (fun _ -> level_of_type c))
-	splayed_lc lc in
+      array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in
     let nf_lc,user_lc = if nf_lc = lc then lc,None else nf_lc, Some lc in
     { mind_consnames = Array.of_list cnames;
       mind_typename = id;
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 46c0255a2..00e108460 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -60,7 +60,7 @@ val mind_check_arities : env -> mutual_inductive_entry -> unit
 
 val cci_inductive : 
   env -> env -> path_kind -> int -> bool -> 
-   (identifier * typed_type * identifier list * bool * bool * typed_type array)
+   (identifier * types * identifier list * bool * bool * types array)
       list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 72058f62c..94a8cc277 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -84,7 +84,7 @@ let mis_type_mconstruct i mispec =
   and nconstr = mis_nconstr mispec in
   let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
-  typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
+  type_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
 
 let mis_user_arity mis =
   let hyps = mis.mis_mib.mind_hyps 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e2d89cdef..054a7d3fe 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -43,11 +43,11 @@ val mis_is_recursive_subset : int list -> inductive_instance -> bool
 val mis_is_recursive : inductive_instance -> bool
 val mis_consnames : inductive_instance -> identifier array
 val mis_inductive : inductive_instance -> inductive
-val mis_nf_arity : inductive_instance -> typed_type
-val mis_user_arity : inductive_instance -> typed_type
+val mis_nf_arity : inductive_instance -> types
+val mis_user_arity : inductive_instance -> types
 val mis_params_ctxt : inductive_instance -> rel_context
 val mis_sort : inductive_instance -> sorts
-val mis_type_mconstruct : int -> inductive_instance -> typed_type
+val mis_type_mconstruct : int -> inductive_instance -> types
 val mis_finite : inductive_instance -> bool 
 
 (* The ccl of constructor is pre-normalised in the following functions *)
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index ab818d0e5..e6a25e6a3 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -26,7 +26,7 @@ let instantiate_constr sign c args =
     replace_vars inst c
 
 let instantiate_type sign tty args =
-  typed_app (fun c -> instantiate_constr sign c args) tty
+  type_app (fun c -> instantiate_constr sign c args) tty
 
 (* Constants. *)
 
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index f905ca27e..0320c4454 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -14,7 +14,7 @@ open Environ
 val instantiate_constr : 
   named_context -> constr -> constr list -> constr
 val instantiate_type : 
-  named_context -> typed_type -> constr list -> typed_type
+  named_context -> types -> constr list -> types
 
 (*s [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
@@ -24,7 +24,7 @@ type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_value : env -> constant -> constr
-val constant_type : env -> 'a evar_map -> constant -> typed_type
+val constant_type : env -> 'a evar_map -> constant -> types
 val constant_opt_value : env -> constant -> constr option
 
 (*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3306927d6..539426bc3 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -975,7 +975,7 @@ let splay_prod env sigma =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
       | IsProd (n,a,c0) ->
-	  decrec (push_rel_assum (n,outcast_type a) env)
+	  decrec (push_rel_assum (n,a) env)
 	    ((n,a)::m) c0
       | _ -> m,t
   in 
@@ -986,11 +986,11 @@ let splay_prod_assum env sigma =
     let t = whd_betadeltaiota_nolet env sigma c in
     match kind_of_term c with
     | IsProd (x,t,c)  ->
-	prodec_rec (push_rel_assum (x,outcast_type t) env)
-	  (Sign.add_rel_assum (x,outcast_type t) l) c
+	prodec_rec (push_rel_assum (x,t) env)
+	  (Sign.add_rel_assum (x, t) l) c
     | IsLetIn (x,b,t,c) ->
-	prodec_rec (push_rel_def (x,b,outcast_type t) env)
-	  (Sign.add_rel_def (x,b,outcast_type t) l) c
+	prodec_rec (push_rel_def (x,b, t) env)
+	  (Sign.add_rel_def (x,b, t) l) c
     | IsCast (c,_)    -> prodec_rec env l c
     | _               -> l,t
   in
@@ -1008,7 +1008,6 @@ let decomp_n_prod env sigma n =
   let rec decrec env m ln c = if m = 0 then (ln,c) else 
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | IsProd (n,a,c0) ->
-	  let a = make_typed_lazy a (fun _ -> Type dummy_univ) in
 	  decrec (push_rel_assum (n,a) env)
 	    (m-1) (Sign.add_rel_assum (n,a) ln) c0
       | _                      -> error "decomp_n_prod: Not enough products"
@@ -1078,8 +1077,8 @@ let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
-      | IsProd (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0
-      | IsLambda (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0
+      | IsProd (x,t,c0) -> decrec (push_rel_assum (x,t) env) c0
+      | IsLambda (x,t,c0) -> decrec (push_rel_assum (x,t) env) c0
       | t -> t
   in 
   decrec env
@@ -1135,12 +1134,12 @@ let poly_args env sigma t =
     match kind_of_term (whd_betadeltaiota env sigma t) with
       | IsProd (x,a,b) ->
 	  add_free_rels_until n a
-	    (aux (push_rel_assum (x,outcast_type a) env) (n+1) b)
+	    (aux (push_rel_assum (x,a) env) (n+1) b)
       | _ -> Intset.empty
   in 
   match kind_of_term (whd_betadeltaiota env sigma t) with 
     | IsProd (x,a,b) ->
-	Intset.elements (aux (push_rel_assum (x,outcast_type a) env) 1 b)
+	Intset.elements (aux (push_rel_assum (x,a) env) 1 b)
     | _ -> []
 
 (* Expanding existential variables (pretyping.ml) *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a62bc962a..7b7c95d4b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -22,7 +22,7 @@ let j_val j = j.uj_val
 let j_type j = body_of_type j.uj_type
 
 let vect_lift = Array.mapi lift
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
 (*s The machine flags. 
    [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$)
@@ -113,7 +113,7 @@ let rec execute mf env cstr =
      | IsProd (name,c1,c2) ->
         let (j,cst1) = execute mf env c1 in
         let varj = type_judgment env Evd.empty j in
-	let env1 = push_rel_assum (name,assumption_of_type_judgment varj) env in
+	let env1 = push_rel_assum (name,varj.utj_val) env in
         let (j',cst2) = execute mf env1 c2 in
 	let (j,cst3) = gen_rel env1 Evd.empty name varj j' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
@@ -122,18 +122,21 @@ let rec execute mf env cstr =
      | IsLetIn (name,c1,c2,c3) ->
         let (j1,cst1) = execute mf env c1 in
         let (j2,cst2) = execute mf env c2 in
-	let { uj_val = b; uj_type = t } = cast_rel env Evd.empty j1 j2 in
+	let tj2 = assumption_of_judgment env Evd.empty j2 in
+	let ({uj_val = b; uj_type = t},cst0) = cast_rel env Evd.empty j1 tj2 in
         let (j3,cst3) = execute mf (push_rel_def (name,b,t) env) c3 in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
-	({ uj_val = mkLetIn (name, j1.uj_val, j2.uj_val, j3.uj_val) ;
-	   uj_type = typed_app (subst1 j1.uj_val) j3.uj_type },
-	 cst)
+	({ uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ;
+	   uj_type = type_app (subst1 j1.uj_val) j3.uj_type },
+	 Constraint.union cst cst0)
 	  
     | IsCast (c,t) ->
         let (cj,cst1) = execute mf env c in
         let (tj,cst2) = execute mf env t in
+	let tj = assumption_of_judgment env Evd.empty tj in
 	let cst = Constraint.union cst1 cst2 in
-        (cast_rel env Evd.empty cj tj, cst)
+	let (j, cst0) = cast_rel env Evd.empty cj tj in
+	(j, Constraint.union cst cst0)
 	  
     | IsXtra _ -> anomaly "Safe_typing: found an Extra"
 	  
@@ -145,7 +148,7 @@ and execute_fix mf env lar lfi vdef =
   let env1 = 
     List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in
   let (vdefj,cst2) = execute_array mf env1 vdef in
-  let vdefv = Array.map j_val_only vdefj in
+  let vdefv = Array.map j_val vdefj in
   let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in
   let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
   (lara,vdefv,cst)
@@ -273,7 +276,7 @@ let add_constant_with_value sp body typ env =
   let (env'',ty,cst') = 
     match typ with
       | None -> 
-	  env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty
+	  env', jb.uj_type, Constraint.empty
       | Some ty -> 
 	  let (jt,cst') = safe_infer env ty in
 	  let env'' = add_constraints cst' env' in
@@ -352,8 +355,7 @@ let rec infos_and_sort env t =
   match kind_of_term t with
     | IsProd (name,c1,c2) ->
         let (varj,_) = safe_infer_type env c1 in
-	let var = assumption_of_type_judgment varj in
-	let env1 = Environ.push_rel_assum (name,var) env in
+	let env1 = Environ.push_rel_assum (name,varj.utj_val) env in
 	let s1 = varj.utj_type in
 	let logic = not (is_info_type env Evd.empty varj) in
 	let small = is_small s1 in
@@ -403,7 +405,7 @@ let type_one_constructor env_ar nparams arsort c =
      global parameters (which add a priori more constraints on their sort) *)
   let cst2 = enforce_type_constructor arsort j.utj_type cst in
 
-  (infos, assumption_of_type_judgment j, cst2)
+  (infos, j.utj_val, cst2)
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
   let arsort = sort_of_arity env_ar ar in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a07be1fca..89e3fbbb7 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -45,9 +45,9 @@ val add_constraints : constraints -> safe_environment -> safe_environment
 
 val pop_named_decls : identifier list -> safe_environment -> safe_environment
 
-val lookup_named : identifier -> safe_environment -> constr option * typed_type
+val lookup_named : identifier -> safe_environment -> constr option * types
 (*i
-val lookup_rel : int -> safe_environment -> name * typed_type
+val lookup_rel : int -> safe_environment -> name * types
 i*)
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
@@ -70,10 +70,10 @@ val safe_infer : safe_environment -> constr -> judgment * constraints
 
 (*i For debug
 val fix_machine : safe_environment -> constr -> judgment * constraints
-val fix_machine_type : safe_environment -> constr -> typed_type * constraints
+val fix_machine_type : safe_environment -> constr -> types * constraints
 
 val unsafe_infer : safe_environment -> constr -> judgment * constraints
-val unsafe_infer_type : safe_environment -> constr -> typed_type * constraints
+val unsafe_infer_type : safe_environment -> constr -> types * constraints
 
 val type_of : safe_environment -> constr -> constr
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 4a8078ef4..eb2763645 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -9,12 +9,12 @@ open Term
 (* Signatures *)
 
 let add d sign = d::sign
-let map f = List.map (fun (na,c,t) -> (na,option_app f c,typed_app f t))
+let map f = List.map (fun (na,c,t) -> (na,option_app f c,type_app f t))
 
 let add_decl (n,t) sign = (n,None,t)::sign
 let add_def (n,c,t) sign = (n,Some c,t)::sign
 
-type named_declaration = identifier * constr option * typed_type
+type named_declaration = identifier * constr option * types
 type named_context = named_declaration list
 
 let add_named_decl = add
@@ -47,7 +47,7 @@ let fold_named_context_reverse = List.fold_left
 let fold_named_context_both_sides = list_fold_right_and_left
 let it_named_context_quantifier f = List.fold_left (fun c d -> f d c)
 
-type rel_declaration = name * constr option * typed_type
+type rel_declaration = name * constr option * types
 type rel_context = rel_declaration list
 
 let add_rel_decl = add
@@ -79,7 +79,7 @@ let rel_context_length = List.length
 let lift_rel_context n sign =
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_app (liftn n k) c,typed_app (liftn n k) t)
+	(na,option_app (liftn n k) c,type_app (liftn n k) t)
 	::(liftrec (k-1) sign)
     | [] -> []
   in
@@ -149,8 +149,8 @@ let empty_names_context = []
 let decompose_prod_assum = 
   let rec prodec_rec l c =
     match kind_of_term c with
-    | IsProd (x,t,c)  -> prodec_rec (add_rel_assum (x,outcast_type t) l) c
-    | IsLetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,outcast_type t) l) c
+    | IsProd (x,t,c)  -> prodec_rec (add_rel_assum (x,t) l) c
+    | IsLetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,t) l) c
     | IsCast (c,_)    -> prodec_rec l c
     | _               -> l,c
   in 
@@ -161,8 +161,8 @@ let decompose_prod_assum =
 let decompose_lam_assum = 
   let rec lamdec_rec l c =
     match kind_of_term c with
-    | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,outcast_type t) l) c
-    | IsLetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,outcast_type t) l) c
+    | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) c
+    | IsLetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,t) l) c
     | IsCast (c,_)     -> lamdec_rec l c
     | _                -> l,c
   in 
@@ -175,9 +175,9 @@ let decompose_prod_n_assum n =
   let rec prodec_rec l n c = 
     if n=0 then l,c 
     else match kind_of_term c with 
-    | IsProd (x,t,c) -> prodec_rec (add_rel_assum(x,outcast_type t) l) (n-1) c
+    | IsProd (x,t,c) -> prodec_rec (add_rel_assum(x,t) l) (n-1) c
     | IsLetIn (x,b,t,c) ->
-	prodec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c
+	prodec_rec (add_rel_def (x,b,t) l) (n-1) c
     | IsCast (c,_)   -> prodec_rec l n c
     | c -> error "decompose_prod_n: not enough products"
   in 
@@ -190,9 +190,9 @@ let decompose_lam_n_assum n =
   let rec lamdec_rec l n c = 
     if n=0 then l,c 
     else match kind_of_term c with 
-    | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,outcast_type t) l) (n-1) c
+    | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,t) l) (n-1) c
     | IsLetIn (x,b,t,c) ->
-	lamdec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c
+	lamdec_rec (add_rel_def (x,b,t) l) (n-1) c
     | IsCast (c,_)     -> lamdec_rec l n c
     | c -> error "decompose_lam_n: not enough abstractions"
   in 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 51e810744..29edde8f6 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -12,12 +12,12 @@ open Term
 type named_context = named_declaration list
 
 val add_named_decl : 
-  identifier * constr option * typed_type -> named_context -> named_context
-val add_named_assum : identifier * typed_type -> named_context -> named_context
+  identifier * constr option * types -> named_context -> named_context
+val add_named_assum : identifier * types -> named_context -> named_context
 val add_named_def : 
-  identifier * constr * typed_type -> named_context -> named_context
-val lookup_id : identifier -> named_context -> constr option * typed_type
-val lookup_id_type : identifier -> named_context -> typed_type
+  identifier * constr * types -> named_context -> named_context
+val lookup_id : identifier -> named_context -> constr option * types
+val lookup_id_type : identifier -> named_context -> types
 val lookup_id_value : identifier -> named_context -> constr option 
 val pop_named_decl : identifier -> named_context -> named_context
 val empty_named_context : named_context
@@ -41,12 +41,12 @@ val keep_hyps : Idset.t -> named_context -> named_context
 
 type rel_context = rel_declaration list
 
-val add_rel_decl : (name * constr option * typed_type) -> rel_context -> rel_context
-val add_rel_assum : (name * typed_type) -> rel_context -> rel_context
-val add_rel_def : (name * constr * typed_type) -> rel_context -> rel_context
-val lookup_rel_type : int -> rel_context -> name * typed_type
+val add_rel_decl : (name * constr option * types) -> rel_context -> rel_context
+val add_rel_assum : (name * types) -> rel_context -> rel_context
+val add_rel_def : (name * constr * types) -> rel_context -> rel_context
+val lookup_rel_type : int -> rel_context -> name * types
 val lookup_rel_value : int -> rel_context -> constr option
-val lookup_rel_id : identifier -> rel_context -> int * typed_type
+val lookup_rel_id : identifier -> rel_context -> int * types
 val empty_rel_context : rel_context
 val rel_context_length : rel_context -> int
 val lift_rel_context : int -> rel_context -> rel_context
diff --git a/kernel/term.ml b/kernel/term.ml
index 81fbd9a02..13fbb5de7 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -750,42 +750,22 @@ let compare_constr f c1 c2 =
 
 (*
 type 'a judge = { body : constr; typ : 'a }
-type typed_type = sorts judge
+type types = sorts judge
 
-let make_typed t s = { body = t; typ = s }
-let make_typed_lazy t f = { body = t; typ = f s }
-
-let typed_app f tt = { body = f tt.body; typ = tt.typ }
+let type_app f tt = { body = f tt.body; typ = tt.typ }
 
 let body_of_type ty = ty.body
-let level_of_type t = (t.typ : sorts)
-
-let incast_type tty = mkCast (tty.body, mkSort tty.typ)
-
-let outcast_type c = kind_of_term c with
-  | IsCast (b, s) when isSort s -> {body=b; typ=destSort s}
-  | _ -> anomaly "outcast_type: Not an in-casted type judgement"
-
-let typed_combine f g t u = { f t.body u.body ; g t.typ u.typ}
 *)
 
-type typed_type = constr
-
-let make_typed t s = t
-let make_typed_lazy t f = t
+type types = constr
 
-let typed_app f tt = f tt
+let type_app f tt = f tt
 
 let body_of_type ty = ty
-let level_of_type t = failwith "N'existe plus"
-
-let incast_type tty = tty
-let outcast_type x = x
-let typed_combine f g t u = f t u
 (**)
 
-type named_declaration = identifier * constr option * typed_type
-type rel_declaration = name * constr option * typed_type
+type named_declaration = identifier * constr option * types
+type rel_declaration = name * constr option * types
 
 
 
@@ -959,7 +939,7 @@ let subst1 lam = substl [lam]
 let substl_decl laml (id,bodyopt,typ as d) =
   match bodyopt with
     | None -> (id,None,substl laml typ)
-    | Some body -> (id, Some (substl laml body), typed_app (substl laml) typ)
+    | Some body -> (id, Some (substl laml body), type_app (substl laml) typ)
 let subst1_decl lam = substl_decl [lam]
 
 (* (thin_val sigma) removes identity substitutions from sigma *)
@@ -1624,12 +1604,12 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
     | None -> (id,None,subst_term_occ locs c typ)
     | Some body -> 
 	if locs = [] then
-	  (id,Some (subst_term c body),typed_app (subst_term c) typ)
+	  (id,Some (subst_term c body),type_app (subst_term c) typ)
 	else if List.mem 0 locs then 
 	  d
 	else 
 	  let (nbocc,body') = subst_term_occ_gen locs 1 c body in
-	  let (nbocc',t') = typed_app (subst_term_occ_gen locs nbocc c) typ in
+	  let (nbocc',t') = type_app (subst_term_occ_gen locs nbocc c) typ in
 	  if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
 	    errorlabstrm "subst_term_occ_decl" [< 'sTR "Too few occurences" >];
 	  (id,Some body',t')
@@ -1654,7 +1634,7 @@ let occur_existential c =
 module Htype =
   Hashcons.Make(
     struct
-      type t = typed_type
+      type t = types
       type u = (constr -> constr) * (sorts -> sorts)
 (*
       let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ}
diff --git a/kernel/term.mli b/kernel/term.mli
index 40bc12ce3..4b7dc26f3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -37,23 +37,17 @@ type case_info = int array * case_printing
 
 type constr
 
-type typed_type
+(* [types] is the same as [constr] but is intended to be used where a
+   {\em type} in CCI sense is expected (Rem:plurial form since [type] is a
+   reserved ML keyword) *)
 
-(*s Functions about [typed_type] *)
+type types = constr
 
-val make_typed : constr -> sorts -> typed_type
-val make_typed_lazy : constr -> (constr -> sorts) -> typed_type
+(*s Functions about [types] *)
 
-val typed_app : (constr -> constr) -> typed_type -> typed_type
-val typed_combine : (constr -> constr -> constr) -> (sorts -> sorts -> sorts)
-      -> (typed_type -> typed_type -> typed_type)
+val type_app : (constr -> constr) -> types -> types
 
-val body_of_type : typed_type -> constr
-val level_of_type : typed_type -> sorts
-
-val incast_type : typed_type -> constr
-
-val outcast_type : constr -> typed_type
+val body_of_type : types -> constr
 
 (*s A {\em declaration} has the form (name,body,type). It is either an
     {\em assumption} if [body=None] or a {\em definition} if
@@ -62,8 +56,8 @@ val outcast_type : constr -> typed_type
     (in the latter case, [na] is of type [name] but just for printing
     purpose *)
 
-type named_declaration = identifier * constr option * typed_type
-type rel_declaration = name * constr option * typed_type
+type named_declaration = identifier * constr option * types
+type rel_declaration = name * constr option * types
 
 type arity = rel_declaration list * sorts
 
@@ -101,9 +95,9 @@ type kind_of_term =
   | IsXtra         of string
   | IsSort         of sorts
   | IsCast         of constr * constr
-  | IsProd         of name * constr * constr
-  | IsLambda       of name * constr * constr
-  | IsLetIn        of name * constr * constr * constr
+  | IsProd         of name * types * constr 
+  | IsLambda       of name * types * constr
+  | IsLetIn        of name * constr * types * constr
   | IsApp         of constr * constr array
   | IsEvar         of existential
   | IsConst        of constant
@@ -155,12 +149,12 @@ val implicit_sort : sorts
 val mkCast : constr * constr -> constr
 
 (* Constructs the product $(x:t_1)t_2$ *)
-val mkProd : name * constr * constr -> constr
+val mkProd : name * types * constr -> constr
 val mkNamedProd : identifier -> constr -> constr -> constr
 val mkProd_string : string -> constr -> constr -> constr
 
 (* Constructs the product $(x:t_1)t_2$ *)
-val mkLetIn : name * constr * constr * constr -> constr
+val mkLetIn : name * constr * types * constr -> constr
 val mkNamedLetIn : identifier -> constr -> constr -> constr -> constr
 
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
@@ -179,7 +173,7 @@ val mkNamedProd_wo_LetIn : named_declaration -> constr -> constr
 val mkArrow : constr -> constr -> constr
 
 (* Constructs the abstraction $[x:t_1]t_2$ *)
-val mkLambda : name * constr * constr -> constr
+val mkLambda : name * types * constr -> constr
 val mkNamedLambda : identifier -> constr -> constr -> constr
 
 (* [mkLambda_string s t c] constructs $[s:t]c$ *)
@@ -652,6 +646,6 @@ val hcons_constr:
   ->
     (constr -> constr) *
     (constr -> constr) *
-    (typed_type -> typed_type)
+    (types -> types)
 
 val hcons1_constr : constr -> constr
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f96b0b9a1..5806e3364 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -37,14 +37,14 @@ type type_error =
   | CaseNotInductive of constr * constr
   | NumberBranches of constr * constr * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * typed_type) * unsafe_judgment
+  | Generalization of (name * types) * unsafe_judgment
   | ActualType of constr * constr * constr
   | CantApplyBadType of (int * constr * constr)
       * unsafe_judgment * unsafe_judgment list
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list
   | IllFormedRecBody of guard_error * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
-      * typed_type array
+      * types array
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
   | CantFindCaseType of constr
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index d8031350c..01dbeb535 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -41,14 +41,14 @@ type type_error =
   | CaseNotInductive of constr * constr
   | NumberBranches of constr * constr * int
   | IllFormedBranch of constr * int * constr * constr
-  | Generalization of (name * typed_type) * unsafe_judgment
+  | Generalization of (name * types) * unsafe_judgment
   | ActualType of constr * constr * constr
   | CantApplyBadType of (int * constr * constr)
       * unsafe_judgment * unsafe_judgment list
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list
   | IllFormedRecBody of guard_error * name list * int * constr array
   | IllTypedRecBody of int * name list * unsafe_judgment array 
-      * typed_type array
+      * types array
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
   | CantFindCaseType of constr
@@ -88,7 +88,7 @@ val error_ill_formed_branch :
   path_kind -> env -> constr -> int -> constr -> constr -> 'b
 
 val error_generalization :
-  path_kind -> env -> 'a Evd.evar_map -> name * typed_type -> unsafe_judgment -> 'b
+  path_kind -> env -> 'a Evd.evar_map -> name * types -> unsafe_judgment -> 'b
 
 val error_actual_type :
   path_kind -> env -> constr -> constr -> constr -> 'b
@@ -105,7 +105,7 @@ val error_ill_formed_rec_body :
 
 val error_ill_typed_rec_body  :
   path_kind -> env -> int -> name list -> unsafe_judgment array 
-    -> typed_type array -> 'b
+    -> types array -> 'b
 
 val error_not_inductive : path_kind -> env -> constr -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 927b33e8c..463eb37a6 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -19,14 +19,12 @@ let make_judge v tj =
   { uj_val = v;
     uj_type = tj }
 
-let j_val_only j = j.uj_val
-
-let typed_type_of_judgment env sigma j = j.uj_type
+let j_val j = j.uj_val
 
 (* This should be a type intended to be assumed *)
 let assumption_of_judgment env sigma j =
   match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
-    | IsSort s -> make_typed j.uj_val s
+    | IsSort s -> j.uj_val
     | _ -> error_assumption CCI env j.uj_val
 
 (* This should be a type (a priori without intension to be an assumption) *)
@@ -35,15 +33,13 @@ let type_judgment env sigma j =
     | IsSort s -> {utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type CCI env j
 
-let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
-
 (* Type of a de Bruijn index. *)
 	  
 let relative env sigma n = 
   try
     let (_,typ) = lookup_rel_type n env in
     { uj_val  = mkRel n;
-      uj_type = typed_app (lift n) typ }
+      uj_type = type_app (lift n) typ }
   with Not_found -> 
     error_unbound_rel CCI env sigma n
 
@@ -205,18 +201,18 @@ let type_of_case env sigma ci pj cj lfj =
     type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in
   let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in
   check_branches_message env sigma (cj.uj_val,body_of_type cj.uj_type) (bty,lft);
-  { uj_val  = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val_only lfj);
-    uj_type = make_typed rslty kind }
+  { uj_val  = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
+    uj_type = rslty }
 
 (* Prop and Set *)
 
 let judge_of_prop =
   { uj_val = mkSort prop;
-    uj_type = make_typed (mkSort type_0) type_1 }
+    uj_type = mkSort type_0 }
 
 let judge_of_set =
   { uj_val = mkSort spec;
-    uj_type = make_typed (mkSort type_0) type_1 }
+    uj_type = mkSort type_0 }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
@@ -227,7 +223,7 @@ let judge_of_prop_contents = function
 let judge_of_type u =
   let (uu,uuu,c) = super_super u in
   { uj_val = mkSort (Type u);
-    uj_type = make_typed (mkSort (Type uu)) (Type uuu) },
+    uj_type = mkSort (Type uu) },
   c
 
 let type_of_sort c =
@@ -249,71 +245,67 @@ let sort_of_product domsort rangsort g =
            (* Product rule (Type_i,Type_i,Type_i) *) 
            | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst)
 
-let sort_of_product_without_univ domsort rangsort =
-  match rangsort with
-    | Prop _ -> rangsort
-    | Type u2 ->
-        (match domsort with
-           | Prop _ -> rangsort
-           | Type u1 -> Type dummy_univ)
-
-let generalize_without_universes (_,_,var as d) c =
-  typed_combine
-    (fun _ c -> mkNamedProd_or_LetIn d c)
-    sort_of_product_without_univ
-    var c
-
-let typed_product env name var c =
-  (* Gros hack ! *)
-  let rcst = ref Constraint.empty in
-  let hacked_sort_of_product s1 s2 =
-    let (s,cst) = sort_of_product s1 s2 (universes env) in (rcst:=cst; s) in
-  typed_combine (fun c t -> mkProd (name,c,t)) hacked_sort_of_product var c,
-  !rcst
+(* [abs_rel env sigma name var j] implements the rule
+
+ env, name:typ |- j.uj_val:j.uj_type     env, |- (name:typ)j.uj_type : s
+ -----------------------------------------------------------------------
+          env |- [name:typ]j.uj_val : (name:typ)j.uj_type
+
+  Since all products are defined in the Calculus of Inductive Constructions
+  and no upper constraint exists on the sort $s$, we don't need to compute $s$
+*)
 
 let abs_rel env sigma name var j =
-  let cvar = incast_type var in
-  let typ,cst = typed_product env name var j.uj_type in
-  { uj_val = mkLambda (name, cvar, j.uj_val);
-    uj_type = typ },
-  cst
+  { uj_val = mkLambda (name, var, j.uj_val);
+    uj_type = mkProd (name, var, j.uj_type) },
+  Constraint.empty
 
-(* Type of a product. *)
+(* [gen_rel env sigma name (typ1,s1) j] implements the rule
 
-let gen_rel env sigma name varj j =
-  let var = assumption_of_type_judgment varj in
-  match kind_of_term(whd_betadeltaiota env sigma (body_of_type j.uj_type)) with
+    env |- typ1:s1       env, name:typ |- j.uj_val : j.uj_type
+    -------------------------------------------------------------------------
+         s' >= (s1,s2), env |- (name:typ)j.uj_val : s'
+
+  where j.uj_type is convertible to a sort s2
+*)
+
+let gen_rel env sigma name {utj_val = t1; utj_type = s1} j =
+  match kind_of_term (whd_betadeltaiota env sigma j.uj_type) with
     | IsSort s ->
-	let (s',g) = sort_of_product varj.utj_type s (universes env) in
-	let res_type = mkSort s' in
-	let (res_kind,g') = type_of_sort res_type in
-        { uj_val = mkProd (name, incast_type var, j.uj_val);
-          uj_type = make_typed res_type res_kind },
-	g'
+	let (s',g) = sort_of_product s1 s (universes env) in
+        { uj_val = mkProd (name, t1, j.uj_val);
+          uj_type = mkSort s' },
+	g
     | _ -> 
 (* 	if is_small (level_of_type j.uj_type) then (* message historique ?? *)
 	  error "Proof objects can only be abstracted" 
 	else
 *)
-	  error_generalization CCI env sigma (name,var) j
+	  error_generalization CCI env sigma (name,t1) j
 
-(* Type of a cast. *)
+(* [cast_rel env sigma (typ1,s1) j] implements the rule
+
+    env, sigma |- cj.uj_val:cj.uj_type    cst, env, sigma |- cj.uj_type = t
+    ---------------------------------------------------------------------
+         cst, env, sigma |- cj.uj_val:t
+*)
 	    
-let cast_rel env sigma cj tj =
-  let tj = assumption_of_judgment env sigma tj in
-  if is_conv_leq env sigma (body_of_type cj.uj_type) (body_of_type tj) then
-    { uj_val = j_val_only cj;
-      uj_type = tj }
-  else 
-    error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) (body_of_type tj)
+let cast_rel env sigma cj t =
+  try 
+    let cst = conv_leq env sigma (body_of_type cj.uj_type) t in
+    { uj_val = j_val cj;
+      uj_type = t },
+    cst
+  with NotConvertible ->
+    error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) t
 
 (* Type of an application. *)
 
 let apply_rel_list env sigma nocheck argjl funj =
   let rec apply_rec n typ cst = function
     | [] -> 
-	{ uj_val  = applist (j_val_only funj, List.map j_val_only argjl);
-          uj_type = typed_app (fun _ -> typ) funj.uj_type },
+	{ uj_val  = applist (j_val funj, List.map j_val argjl);
+          uj_type = type_app (fun _ -> typ) funj.uj_type },
 	cst
     | hj::restjl ->
         match kind_of_term (whd_betadeltaiota env sigma typ) with
@@ -368,13 +360,13 @@ let check_term env mind_recvec f =
     match lrec, kind_of_term (strip_outer_cast c) with
       | (Param(_)::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
-          crec (push_rel_assum (x,outcast_type a) env) (n+1) l' (lr,b)
+          crec (push_rel_assum (x,a) env) (n+1) l' (lr,b)
       | (Norec::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
-          crec (push_rel_assum (x,outcast_type a) env) (n+1) l' (lr,b)
+          crec (push_rel_assum (x,a) env) (n+1) l' (lr,b)
       | (Mrec(i)::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
-          crec (push_rel_assum (x,outcast_type a) env) (n+1)
+          crec (push_rel_assum (x, a) env) (n+1)
 	    ((1,mind_recvec.(i))::l') (lr,b)
       | (Imbr((sp,i) as ind_sp,lrc)::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
@@ -383,7 +375,7 @@ let check_term env mind_recvec f =
           let lc = 
 	    Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
 	  in
-          crec (push_rel_assum (x,outcast_type a) env) (n+1) ((1,lc)::l') (lr,b)
+          crec (push_rel_assum (x, a) env) (n+1) ((1,lc)::l') (lr,b)
       | _,_ -> f env n l (strip_outer_cast c)
   in 
   crec env
@@ -444,7 +436,7 @@ let is_subterm_specif env sigma lcx mind_recvec =
 	    
       | IsLambda (x,a,b) when l=[] -> 
           let lst' = map_lift_fst lst in
-          crec (push_rel_assum (x,outcast_type a) env) (n+1) lst' b
+          crec (push_rel_assum (x, a) env) (n+1) lst' b
 
       (*** Experimental change *************************)
       | IsMeta _ -> [||]
@@ -473,7 +465,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
      match kind_of_term (strip_outer_cast def) with
        | IsLambda (x,a,b) -> 
 	   if noccur_with_meta n nfi a then
-	     let env' = push_rel_assum (x,outcast_type a) env in
+	     let env' = push_rel_assum (x, a) env in
              if n = k+1 then (env',a,b)
 	     else check_occur env' (n+1) b
            else 
@@ -581,20 +573,20 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 
 	| IsLambda (x,a,b) -> 
 	    (check_rec_call env n lst a) &&
-            (check_rec_call (push_rel_assum (x,outcast_type a) env)
+            (check_rec_call (push_rel_assum (x, a) env)
 	       (n+1) (map_lift_fst lst) b) &&
             (List.for_all (check_rec_call env n lst) l)
 
 	| IsProd (x,a,b) -> 
 	    (check_rec_call env n lst a) &&
-            (check_rec_call (push_rel_assum (x,outcast_type a) env)
+            (check_rec_call (push_rel_assum (x, a) env)
 	       (n+1) (map_lift_fst lst) b) &&
             (List.for_all (check_rec_call env n lst) l)
 
 	| IsLetIn (x,a,b,c) -> 
 	    (check_rec_call env n lst a) &&
 	    (check_rec_call env n lst b) &&
-            (check_rec_call (push_rel_def (x,a,outcast_type b) env)
+            (check_rec_call (push_rel_def (x,a, b) env)
 	       (n+1) (map_lift_fst lst) c) &&
             (List.for_all (check_rec_call env n lst) l)
 
@@ -643,7 +635,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	    | IsLambda (x,a,b) ->
 		(check_rec_call env n lst a) &
 		(check_rec_call_fix_body
-		   (push_rel_assum (x,outcast_type a) env) (n+1)
+		   (push_rel_assum (x, a) env) (n+1)
 		   (map_lift_fst lst) (decr-1) recArgsDecrArg b)
 	    | _ -> anomaly "Not enough abstractions in fix body"
     
@@ -683,7 +675,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
     let b = whd_betadeltaiota env sigma (strip_outer_cast c) in
     match kind_of_term b with
       | IsProd (x,a,b) ->
-	  codomain_is_coind (push_rel_assum (x,outcast_type a) env) b 
+	  codomain_is_coind (push_rel_assum (x, a) env) b 
       | _ -> 
 	  try
 	    find_coinductive env sigma b
@@ -756,7 +748,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
 	| IsLambda (x,a,b) ->
 	     assert (args = []);
             if (noccur_with_meta n nbfix a) then
-              check_rec_call (push_rel_assum (x,outcast_type a) env)
+              check_rec_call (push_rel_assum (x, a) env)
 		alreadygrd (n+1)  vlra b
             else 
 	      raise (CoFixGuardError (RecCallInTypeOfAbstraction t))
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 9c4d62b95..9f2bde9b8 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -13,29 +13,26 @@ open Environ
 
 (* Basic operations of the typing machine. *)
 
-val make_judge : constr -> typed_type -> unsafe_judgment
+val make_judge : constr -> types -> unsafe_judgment
 
-val j_val_only : unsafe_judgment -> constr
+val j_val : unsafe_judgment -> constr
 
-(* If [j] is the judgement $c:t:s$, then [typed_type_of_judgment env j]
-   constructs the typed type $t:s$, while [assumption_of_judgement env j]
-   cosntructs the type type $c:t$, checking that $t$ is a sort. *)
+(* If [j] is the judgement $c:t$, then [assumption_of_judgement env j]
+   returns the type $c$, checking that $t$ is a sort. *)
 
-val typed_type_of_judgment : 
-  env -> 'a evar_map -> unsafe_judgment -> typed_type
 val assumption_of_judgment : 
-  env -> 'a evar_map -> unsafe_judgment -> typed_type
-val assumption_of_type_judgment : unsafe_type_judgment -> typed_type
+  env -> 'a evar_map -> unsafe_judgment -> types
+
 val type_judgment : 
   env -> 'a evar_map -> unsafe_judgment -> unsafe_type_judgment
 
 val relative : env -> 'a evar_map -> int -> unsafe_judgment
 
-val type_of_constant : env -> 'a evar_map -> constant -> typed_type
+val type_of_constant : env -> 'a evar_map -> constant -> types
 
-val type_of_inductive : env -> 'a evar_map -> inductive -> typed_type
+val type_of_inductive : env -> 'a evar_map -> inductive -> types
 
-val type_of_constructor : env -> 'a evar_map -> constructor -> typed_type
+val type_of_constructor : env -> 'a evar_map -> constructor -> types
 
 val type_of_existential : env -> 'a evar_map -> constr -> constr
 
@@ -51,22 +48,22 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 
 val judge_of_type : universe -> unsafe_judgment * constraints
 
-val generalize_without_universes : named_declaration -> typed_type -> typed_type
-
+(*s Type of an abstraction. *)
 val abs_rel : 
-  env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
+  env -> 'a evar_map -> name -> types -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
+(*s Type of a product. *)
 val gen_rel :
   env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val sort_of_product : sorts -> sorts -> universes -> sorts * constraints
-val sort_of_product_without_univ : sorts -> sorts -> sorts
 
-val cast_rel : 
-  env -> 'a evar_map -> unsafe_judgment -> unsafe_judgment 
-    -> unsafe_judgment
+(*s Type of a cast. *)
+val cast_rel :
+  env -> 'a evar_map -> unsafe_judgment -> types
+    -> unsafe_judgment * constraints
 
 val apply_rel_list : 
   env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment
@@ -76,7 +73,7 @@ val check_fix : env -> 'a evar_map -> fixpoint -> unit
 val check_cofix : env -> 'a evar_map -> cofixpoint -> unit
 val control_only_guard : env -> 'a evar_map -> constr -> unit
 
-val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array 
+val type_fixpoint : env -> 'a evar_map -> name list -> types array 
     -> unsafe_judgment array -> constraints
 
 open Inductive
diff --git a/library/global.mli b/library/global.mli
index 88f690c54..e9a9503ff 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -33,8 +33,8 @@ val add_constraints : constraints -> unit
 
 val pop_named_decls : identifier list -> unit
 
-val lookup_named : identifier -> constr option * typed_type
-(*i val lookup_rel : int -> name * typed_type i*)
+val lookup_named : identifier -> constr option * types
+(*i val lookup_rel : int -> name * types i*)
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : inductive -> inductive_instance
diff --git a/library/indrec.ml b/library/indrec.ml
index 6f1a4cd12..a11ca751b 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -173,19 +173,19 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
         (match optionpos with 
            | None -> 
 	       lambda_name env
-		 (n,incast_type t,process_constr (i+1)
+		 (n,t,process_constr (i+1)
 		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
 		    (cprest,rest))
            | Some(_,f_0) -> 
 	       let nF = lift (i+1+decF) f_0 in
 	       let arg = process_pos nF (lift 1 (body_of_type t)) in 
                lambda_name env
-		 (n,incast_type t,process_constr (i+1)
+		 (n,t,process_constr (i+1)
 		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
     | (n,Some c,t)::cprest, rest ->
 	       mkLetIn
-		 (n,c,incast_type t,
+		 (n,c,t,
 		  process_constr (i+1) (lift 1 f) (cprest,rest))
     | [],[] -> f
     | _,[] | [],_ -> anomaly "process_constr"
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 176a3c3e9..413ea152a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -135,11 +135,7 @@ let inductive_of_rawconstructor c =
   inductive_of_constructor (constructor_of_rawconstructor c)
 
 (* Environment management *)
-let push_rel_type sigma (na,t) env =
-  push_rel_assum (na,get_assumption_of env sigma t) env
-
-let push_rels vars env =
-  List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env
+let push_rels vars env = List.fold_right push_rel_assum vars env
 
 (**********************************************************************)
 (* Structures used in compiling pattern-matching *)
@@ -670,8 +666,7 @@ let abstract_predicate env sigma indf = function
       let dep = copt <> None in
       let sign' =
 	if dep then
-	  let ind=get_assumption_of env sigma (build_dependent_inductive indf)
-	  in (Anonymous,None,ind)::sign
+	  (Anonymous,None,build_dependent_inductive indf) :: sign
 	else sign in
       (dep, it_mkLambda_or_LetIn_name env (extract_predicate pred) sign')
 
@@ -764,7 +759,7 @@ let build_branch pb defaults eqns const_info =
   let _,typs' =
     List.fold_right
       (fun (na,t) (env,typs) ->
- 	 (push_rel_assum (na,outcast_type t) env,
+ 	 (push_rel_assum (na,t) env,
 	  ((na,to_mutind env !(pb.isevars) t),t)::typs))
       typs (pb.env,[]) in
   let tomatchs =
@@ -834,7 +829,7 @@ and match_current pb (n,tm) =
 	      pb.pred brtyps cstrs current indt in
 	  let ci = make_case_info mis None tags in
 	  { uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)pred,current,brvals);
-	    uj_type = make_typed typ s }
+	    uj_type = typ }
 
 and compile_further pb firstnext rest =
   (* We pop as much as possible tomatch not dependent one of the other *)
@@ -855,7 +850,7 @@ and compile_further pb firstnext rest =
   let j = compile pb' in
   { uj_val = lam_it j.uj_val sign;
     uj_type = (* Pas d'univers ici: imprédicatif si Prop/Set, dummy si Type *)
-      typed_app (fun t -> prod_it t sign) j.uj_type }
+      type_app (fun t -> prod_it t sign) j.uj_type }
 
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -923,9 +918,8 @@ let inh_coerce_to_ind isevars env ty tyi =
   let (_,evarl) =
     List.fold_right
       (fun (na,ty) (env,evl) ->
-	 let aty = get_assumption_of env Evd.empty ty in
-	   (push_rel_assum (na,aty) env,
-	    (new_isevar isevars env (incast_type aty) CCI)::evl))
+	 (push_rel_assum (na,ty) env,
+	    (new_isevar isevars env ty CCI)::evl))
       ntys (env,[]) in
   let expected_typ = applist (mkMutInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
@@ -1105,7 +1099,5 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
   let j = compile pb in
   
   match tycon with
-    | Some p ->
-	let p = get_assumption_of env !isevars p in
-	Coercion.inh_conv_coerce_to loc env isevars j p
+    | Some p ->	Coercion.inh_conv_coerce_to loc env isevars j p
     | None -> j
diff --git a/pretyping/class.ml b/pretyping/class.ml
index b83eb3608..0f201d004 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -285,14 +285,12 @@ lorque source est None alors target est None aussi.
 let try_add_new_coercion_core idf stre source target isid =
   let env = Global.env () in
   let v = construct_reference env CCI idf in
-  let t = Retyping.get_type_of env Evd.empty v in
-  let k = Retyping.get_sort_of env Evd.empty t in
-  let vj = {uj_val=v; uj_type= make_typed t k} in
+  let vj = Retyping.get_judgment_of env Evd.empty v in
   let f_vardep,coef = coe_of_reference v in
   if coercion_exists coef then
     errorlabstrm "try_add_coercion" 
       [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
-  let lp = prods_of t in
+  let lp = prods_of (vj.uj_type) in
   let llp = List.length lp in
   if llp <= 1 then
     errorlabstrm "try_add_coercion"         
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9040ce3eb..a4dfa3683 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -19,15 +19,15 @@ let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t)
 
 let j_nf_ise env sigma {uj_val=v;uj_type=t} =
   { uj_val = nf_ise1 sigma v; 
-    uj_type = typed_app (nf_ise1 sigma) t }
+    uj_type = nf_ise1 sigma t }
 
 let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
 
 (* Here, funj is a coercion therefore already typed in global context *)
 let apply_coercion_args env argl funj =
   let rec apply_rec acc typ = function
-    | [] -> { uj_val=applist(j_val_only funj,argl);
-              uj_type= typed_app (fun _ -> typ) funj.uj_type }
+    | [] -> { uj_val = applist (j_val funj,argl);
+              uj_type = typ }
     | h::restl ->
       (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
   	match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
@@ -36,11 +36,13 @@ let apply_coercion_args env argl funj =
 	      apply_rec (h::acc) (subst1 h c2) restl
 	  | _ -> anomaly "apply_coercion_args"
   in 
-  apply_rec [] (body_of_type funj.uj_type) argl
+  apply_rec [] funj.uj_type argl
 
 (* appliquer le chemin de coercions p a` hj *)
 
-let apply_pcoercion env p hj typ_cl =
+exception NoCoercion
+
+let apply_coercion env p hj typ_cl =
   if !compter then begin
     nbpathc := !nbpathc +1; 
     nbcoer := !nbcoer + (List.length p)
@@ -48,79 +50,74 @@ let apply_pcoercion env p hj typ_cl =
   try 
     fst (List.fold_left
            (fun (ja,typ_cl) i -> 
-              let fv,b= coe_value i in
+              let fv,b = coe_value i in
               let argl = (class_args_of typ_cl)@[ja.uj_val] in
               let jres = apply_coercion_args env argl fv in
               (if b then 
 		 { uj_val=ja.uj_val; uj_type=jres.uj_type }
                else 
 		 jres),
-	      (body_of_type jres.uj_type))
+	      jres.uj_type)
            (hj,typ_cl) p)
-  with _ -> anomaly "apply_pcoercion"
+  with _ -> anomaly "apply_coercion"
 
 let inh_app_fun env isevars j = 
-  let t = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
+  let t = whd_betadeltaiota env !isevars j.uj_type in
   match kind_of_term t with
     | IsProd (_,_,_) -> j
     | _ ->
        	(try
- 	   let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
+ 	   let t,i1 = class_of1 env !isevars j.uj_type in
       	   let p = lookup_path_to_fun_from i1 in
-           apply_pcoercion env p j t
+           apply_coercion env p j t
 	 with Not_found -> j)
 
 let inh_tosort_force env isevars j =
   try
-    let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
+    let t,i1 = class_of1 env !isevars j.uj_type in
     let p = lookup_path_to_sort_from i1 in
-    apply_pcoercion env p j t 
+    apply_coercion env p j t 
   with Not_found -> 
     j
 
 let inh_tosort env isevars j = 
-  let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
+  let typ = whd_betadeltaiota env !isevars j.uj_type in
   match kind_of_term typ with
     | IsSort _ -> j  (* idem inh_app_fun *)
     | _ -> inh_tosort_force env isevars j
 
 let inh_ass_of_j env isevars j =
-  let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
+  let typ = whd_betadeltaiota env !isevars j.uj_type in
   match kind_of_term typ with
     | IsSort s -> { utj_val = j.uj_val; utj_type = s }
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
 	type_judgment env !isevars j1 
 
-exception NoCoercion
-
 let inh_coerce_to_fail env isevars c1 hj =
   let hj' =
     try 
       let t1,i1 = class_of1 env !isevars c1 in
-      let t2,i2 = class_of1 env !isevars (body_of_type hj.uj_type) in
+      let t2,i2 = class_of1 env !isevars hj.uj_type in
       let p = lookup_path_between (i2,i1) in
-      apply_pcoercion env p hj t2
+      apply_coercion env p hj t2
     with Not_found -> raise NoCoercion 
   in
-  if the_conv_x_leq env isevars (body_of_type hj'.uj_type) c1 then 
+  if the_conv_x_leq env isevars hj'.uj_type c1 then 
     hj'
   else
     raise NoCoercion
 
 let rec inh_conv_coerce_to_fail env isevars c1 hj =
   let {uj_val = v; uj_type = t} = hj in
-  let t = body_of_type t in
   if the_conv_x_leq env isevars t c1 then hj
   else 
     try 
       inh_coerce_to_fail env isevars c1 hj
     with NoCoercion ->  (* try ... with _ -> ... is BAD *)
-      (*   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*)
       (match kind_of_term (whd_betadeltaiota env !isevars t),
 	     kind_of_term (whd_betadeltaiota env !isevars c1) with
 	 | IsProd (_,t1,t2), IsProd (name,u1,u2) -> 
- 	     (* let v' = hnf_constr !isevars v in *)
              let v' = whd_betadeltaiota env !isevars v in
              if (match kind_of_term v' with
                    | IsLambda (_,v1,v2) ->
@@ -128,50 +125,48 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
                    | _  -> false)
              then 
 	       let (x,v1,v2) = destLambda v' in
-               (* let jv1 = exemeta_rec def_vty_con env isevars v1 in 
-	          let assv1 = assumption_of_judgement env !isevars jv1 in *)
-	       let assv1 = outcast_type v1 in
-               let env1 = push_rel_assum (x,assv1) env in
+               let env1 = push_rel_assum (x,v1) env in
                let h2 = inh_conv_coerce_to_fail env isevars u2
-			  {uj_val = v2;
-			   uj_type = get_assumption_of env1 !isevars t2 } in
-               fst (abs_rel env !isevars x assv1 h2)
+			  {uj_val = v2; uj_type = t2 } in
+               fst (abs_rel env !isevars x v1 h2)
              else 
-	       let assu1 = get_assumption_of env !isevars u1 in
                let name = (match name with 
 			     | Anonymous -> Name (id_of_string "x")
                              | _ -> name) in
-               let env1 = push_rel_assum (name,assu1) env in
+               let env1 = push_rel_assum (name,u1) env in
                let h1 = 
 		 inh_conv_coerce_to_fail env isevars t1
 		   {uj_val = mkRel 1; 
-		    uj_type = typed_app (fun _ -> u1) assu1 } in
+		    uj_type = u1 } in
                let h2 = inh_conv_coerce_to_fail env isevars u2  
 			 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
-                           uj_type = get_assumption_of env1 !isevars
-				       (subst1 h1.uj_val t2) }
+                           uj_type = subst1 h1.uj_val t2 }
 	       in
-	       fst (abs_rel env !isevars name assu1 h2)
+	       fst (abs_rel env !isevars name u1 h2)
 	 | _ -> raise NoCoercion)
 
-let inh_conv_coerce_to loc env isevars cj tj =
+let inh_conv_coerce_to loc env isevars cj t =
   let cj' = 
     try 
-      inh_conv_coerce_to_fail env isevars (body_of_type tj) cj 
+      inh_conv_coerce_to_fail env isevars t cj 
     with NoCoercion -> 
       let rcj = j_nf_ise env !isevars cj in
-      let at = nf_ise1 !isevars (body_of_type tj) in
-      error_actual_type_loc loc env rcj.uj_val (body_of_type rcj.uj_type) at
+      let at = nf_ise1 !isevars t in
+      error_actual_type_loc loc env rcj.uj_val rcj.uj_type at
   in
   { uj_val = cj'.uj_val;
-    uj_type = tj }
+    uj_type = t }
+
+(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
+   args)] of type [tycon] (if any) by inserting coercions in front of
+   each arg$_i$, if necessary *)
 
-let inh_apply_rel_list nocheck apploc env isevars argjl funj tycon =
+let inh_apply_rel_list apploc env isevars argjl funj tycon =
   let rec apply_rec n acc typ = function
     | [] -> 
 	let resj =
-      	  { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc));
-	    uj_type= typed_app (fun _ -> typ) funj.uj_type } 
+      	  { uj_val = applist (j_val funj, List.rev acc);
+	    uj_type = typ } 
       	in
       	(match tycon with 
 	   | Some typ' ->
@@ -183,22 +178,19 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj tycon =
       	match kind_of_term (whd_betadeltaiota env !isevars typ) with
           | IsProd (_,c1,c2) ->
               let hj' =
-              	if nocheck then 
-		  hj 
-		else 
-		  (try 
-		     inh_conv_coerce_to_fail env isevars c1 hj 
-		   with NoCoercion ->
-                     error_cant_apply_bad_type_loc apploc env 
-		       (n,nf_ise1 !isevars c1,
-			nf_ise1 !isevars (body_of_type hj.uj_type))
-		       (j_nf_ise env !isevars funj)
-		       (jl_nf_ise env !isevars argjl)) 
+		(try 
+		   inh_conv_coerce_to_fail env isevars c1 hj 
+		 with NoCoercion ->
+                   error_cant_apply_bad_type_loc apploc env 
+		     (n,nf_ise1 !isevars c1,
+		      nf_ise1 !isevars hj.uj_type)
+		     (j_nf_ise env !isevars funj)
+		     (jl_nf_ise env !isevars argjl))
 	      in
-              apply_rec (n+1) (hj'::acc) (subst1 hj'.uj_val c2) restjl
+	      apply_rec (n+1) ((j_val hj')::acc) (subst1 hj'.uj_val c2) restjl
           | _ ->
               error_cant_apply_not_functional_loc apploc env
 	      	(j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)
   in 
-  apply_rec 1 [] (body_of_type funj.uj_type) argjl
+  apply_rec 1 [] funj.uj_type argjl
 
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 52cdabc06..0969387fb 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -9,20 +9,30 @@ open Environ
 open Evarutil
 (*i*)
 
-(* Coercions. *)
+(*s Coercions. *)
 
 val inh_app_fun :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_tosort_force :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
+
+(* [inh_tosort env sigma j] insert a coercion into [j], if needed, in
+   such a way [t] reduces to a sort; it fails if no coercion is applicable *)
 val inh_tosort :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
-val inh_ass_of_j : 
+
+val inh_ass_of_j :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
 
+(* [inh_conv_coerce_to loc env sigma j t] insert a coercion into [j],
+   if needed, in such a way it [t] and [j.uj_type] are convertible; it
+   fails if no coercion is applicable *)
 val inh_conv_coerce_to : Rawterm.loc ->
-  env -> 'a evar_defs -> unsafe_judgment -> typed_type -> unsafe_judgment
+  env -> 'a evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
 
-val inh_apply_rel_list : bool -> Rawterm.loc -> env -> 'a evar_defs ->
+(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
+   args)] of type [tycon] (if any) by inserting coercions in front of
+   each arg$_i$, if necessary *)
+val inh_apply_rel_list : Rawterm.loc -> env -> 'a evar_defs ->
   unsafe_judgment list -> unsafe_judgment -> constr option
     -> unsafe_judgment
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f4e9d01b7..15151ca9b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -263,8 +263,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> 
         evar_conv_x env isevars CONV c1 c2
         & 
-	(let d = Retyping.get_assumption_of env !isevars (nf_ise1 !isevars c1)
-	 in evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
+	(let d = nf_ise1 !isevars c1 in
+	 evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
 
     | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
 	sp1=sp2
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 8aac75e39..3f0570dc9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -76,7 +76,7 @@ let split_evar_to_arrow sigma c =
   let (sigma1,dom) = new_type_var evenv sigma in
   let hyps = named_context evenv in
   let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
-  let newenv = push_named_assum (nvar,make_typed dom (Type dummy_univ)) evenv in
+  let newenv = push_named_assum (nvar, dom) evenv in
   let (sigma2,rng) = new_type_var newenv sigma1 in
   let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in
   let sigma3 = Evd.define sigma2 ev prod in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9caab6bcc..ff10083ff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -95,10 +95,10 @@ let ctxt_of_ids cl = cl
 
 let mt_evd = Evd.empty
 
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
 let j_nf_ise sigma {uj_val=v;uj_type=t} =
-  {uj_val=nf_ise1 sigma v;uj_type=typed_app (nf_ise1 sigma) t}
+  {uj_val=nf_ise1 sigma v;uj_type=type_app (nf_ise1 sigma) t}
 
 let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
 
@@ -112,23 +112,13 @@ let evar_type_fixpoint env isevars lna lar vdefj =
     if Array.length lar = lt then 
       for i = 0 to lt-1 do 
         if not (the_conv_x_leq env isevars
-		  (body_of_type (vdefj.(i)).uj_type)
-		  (lift lt (body_of_type lar.(i)))) then
+		  (vdefj.(i)).uj_type
+		  (lift lt lar.(i))) then
           error_ill_typed_rec_body CCI env i lna 
 	    (jv_nf_ise !isevars vdefj) 
-	    (Array.map (typed_app (nf_ise1 !isevars)) lar)
+	    (Array.map (type_app (nf_ise1 !isevars)) lar)
       done
 
-
-(* Inutile ?
-let cast_rel isevars env cj tj =
-    if the_conv_x_leq isevars env cj.uj_type tj.uj_val then
-        {uj_val=j_val_only cj;
-         uj_type=tj.uj_val;
-         uj_kind = hnf_constr !isevars tj.uj_type}
-   else error_actual_type CCI env (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)
-
-*)
 let let_path = make_path ["Core"] (id_of_string "let") CCI
 
 let wrong_number_of_cases_message loc env isevars (c,ct) expn = 
@@ -156,7 +146,7 @@ let pretype_id loc env lvar id =
   with Not_found ->
   try
     let (n,typ) = lookup_rel_id id (rel_context env) in
-    { uj_val  = mkRel n; uj_type = typed_app (lift n) typ }
+    { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
   with Not_found ->
   try
     let typ = lookup_id_type id (named_context env) in
@@ -183,7 +173,7 @@ let pretype_ref pretype loc isevars env lvar = function
 	mkEvar ev
     in
     let typ = existential_type !isevars ev in
-    make_judge body (Retyping.get_assumption_of env !isevars typ)
+    make_judge body typ
 
 | RInd (ind_sp,ctxt) ->
     let ind = (ind_sp,Array.map pretype ctxt) in
@@ -198,7 +188,7 @@ let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
   | RType ->
       { uj_val = dummy_sort;
-	uj_type = make_typed dummy_sort (Type Univ.dummy_univ) }
+	uj_type = dummy_sort }
 
 (* pretype tycon isevars env constr tries to solve the *)
 (* existential variables in constr in environment env with the *)
@@ -223,9 +213,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
   (match tycon with
-  | Some ty ->
-      let c = new_isevar isevars env ty CCI in
-      {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
+  | Some ty -> { uj_val = new_isevar isevars env ty CCI; uj_type = ty }
   | None ->
       (match loc with
 	   None -> anomaly "There is an implicit argument I cannot solve"
@@ -249,14 +237,13 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
         pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars lvar
           lmeta def) vdef in
   (evar_type_fixpoint env isevars lfi lara vdefj;
-   let larav = Array.map body_of_type lara in
    match fixkind with
      | RFix (vn,i as vni) ->
-	 let fix = (vni,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+	 let fix = (vni,(lara,List.rev lfi,Array.map j_val vdefj)) in
 	 check_fix env !isevars fix;
 	 make_judge (mkFix fix) lara.(i)
      | RCoFix i -> 
-	 let cofix = (i,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+	 let cofix = (i,(lara,List.rev lfi,Array.map j_val vdefj)) in
 	 check_cofix env !isevars cofix;
 	 make_judge (mkCoFix cofix) lara.(i))
 
@@ -271,14 +258,14 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       let rng_tycon = option_app (subst1 cj.uj_val) rng in
       (rng_tycon,cj::jl)  in
     let jl = List.rev (snd (List.fold_left apply_one_arg
-			      (mk_tycon (body_of_type j.uj_type),[]) args)) in
-    inh_apply_rel_list false loc env isevars jl j tycon
+			      (mk_tycon j.uj_type,[]) args)) in
+    inh_apply_rel_list loc env isevars jl j tycon
 
 | RBinder(loc,BLambda,name,c1,c2)      ->
     let (dom,rng) = split_tycon loc env isevars tycon in
     let dom_valcon = valcon_of_tycon dom in
     let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
-    let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
+    let assum = (inh_ass_of_j env isevars j).utj_val in
     let var = (name,assum) in
     let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 
     in 
@@ -287,7 +274,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | RBinder(loc,BProd,name,c1,c2)        ->
     let j = pretype empty_tycon env isevars lvar lmeta c1 in
     let assum = inh_ass_of_j env isevars j in
-    let var = (name,assumption_of_type_judgment assum) in
+    let var = (name,assum.utj_val) in
     let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in
     (try fst (gen_rel env !isevars name assum j')
      with TypeError _ as e -> Stdpp.raise_with_loc loc e)
@@ -296,15 +283,15 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     let j = pretype empty_tycon env isevars lvar lmeta c1 in
     let var = (name,j.uj_val,j.uj_type) in
     let j' = pretype tycon (push_rel_def var env) isevars lvar lmeta c2 in
-    { uj_val = mkLetIn (name, j.uj_val, body_of_type j.uj_type, j'.uj_val) ;
-      uj_type = typed_app (subst1 j.uj_val) j'.uj_type }
+    { uj_val = mkLetIn (name, j.uj_val, j.uj_type, j'.uj_val) ;
+      uj_type = type_app (subst1 j.uj_val) j'.uj_type }
 
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype empty_tycon env isevars lvar lmeta c in
   let (IndType (indf,realargs) as indt) = 
-    try find_rectype env !isevars (body_of_type cj.uj_type)
+    try find_rectype env !isevars cj.uj_type
     with Induc -> error_case_not_inductive CCI env
-	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars (body_of_type cj.uj_type)) in
+	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
   let pj = match po with
     | Some p -> pretype empty_tycon env isevars lvar lmeta p
     | None -> 
@@ -323,34 +310,34 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 		let expti = expbr.(i) in
 		let fj =
                   pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
-		let efjt = nf_ise1 !isevars (body_of_type fj.uj_type) in 
+		let efjt = nf_ise1 !isevars fj.uj_type in 
 		let pred = 
 		  Cases.pred_case_ml_onebranch env !isevars isrec indt
 		    (i,fj.uj_val,efjt) in
 		if has_ise !isevars pred then findtype (i+1)
 		else 
 		  let pty = Retyping.get_type_of env !isevars pred in
-		  { uj_val=pred; 
-		    uj_type = Retyping.get_assumption_of env !isevars pty }
+		  { uj_val = pred; 
+		    uj_type = pty }
 	      with UserError _ -> findtype (i+1) in
 	    findtype 0 in
 
-  let evalct = find_rectype env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
-  and evalPt = nf_ise1 !isevars (body_of_type pj.uj_type) in
+  let evalct = find_rectype env !isevars cj.uj_type (*Pour normaliser evars*)
+  and evalPt = nf_ise1 !isevars pj.uj_type in
 
   let (bty,rsty) =
     Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
   if Array.length bty <> Array.length lf then
     wrong_number_of_cases_message loc env isevars 
-      (cj.uj_val,nf_ise1 !isevars (body_of_type cj.uj_type))
+      (cj.uj_val,nf_ise1 !isevars cj.uj_type)
       (Array.length bty)
   else
     let lfj =
       array_map2
         (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar lmeta f) bty
           lf in
-    let lfv = (Array.map (fun j -> j.uj_val) lfj) in
-    let lft = (Array.map (fun j -> body_of_type j.uj_type) lfj) in
+    let lfv = Array.map j_val lfj in
+    let lft = Array.map (fun j -> j.uj_type) lfj in
     check_branches_message loc env isevars cj.uj_val (bty,lft);
     let v =
       if isrec
@@ -361,9 +348,8 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	let ci = make_default_case_info mis in
 	mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map (fun j-> j.uj_val) lfj)
     in
-    let s = snd (splay_arity env !isevars evalPt) in
     {uj_val = v;
-     uj_type = make_typed rsty s }
+     uj_type = rsty }
 
 | RCases (loc,prinfo,po,tml,eqns) ->
     Cases.compile_cases loc
@@ -376,9 +362,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
   let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in
   match tycon with
     | None  -> cj
-    | Some t' -> 
-	let tj' = Retyping.get_assumption_of env !isevars t' in
-	inh_conv_coerce_to loc env isevars cj tj'
+    | Some t' -> inh_conv_coerce_to loc env isevars cj t'
 
 and pretype_type valcon env isevars lvar lmeta = function
 | RHole loc ->
@@ -386,9 +370,8 @@ and pretype_type valcon env isevars lvar lmeta = function
     (match valcon with
        | Some v -> Retyping.get_judgment_of env !isevars v
        | None ->
-	   let ty = dummy_sort in
-	   let c = new_isevar isevars env ty CCI in
-	   { uj_val = c ; uj_type = make_typed ty (Type Univ.dummy_univ) })
+	   { uj_val = new_isevar isevars env dummy_sort CCI;
+	     uj_type = dummy_sort })
 | c ->
   let j = pretype empty_tycon env isevars lvar lmeta c in
   let tj = inh_tosort env isevars j in
@@ -453,7 +436,7 @@ let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
   let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
   let metamap = ref [] in
   let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
-  let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+  let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
   !metamap, {uj_val = v; uj_type = t }
 
 let ise_resolve_casted sigma env typ c =
@@ -468,7 +451,7 @@ let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
   let j = unsafe_infer tycon isevars env lvar lmeta c in
   let metamap = ref [] in
   let v = process_evars fail_evar sigma !isevars metamap j.uj_val in
-  let t = typed_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
+  let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in
   !metamap, {uj_val = v; uj_type = t }
 
 let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4f36fbbdd..53bf5b08a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -63,11 +63,9 @@ let rec type_of env cstr=
 	  then realargs@[c] else realargs in
         whd_betadeltaiota env sigma (applist (p,al))
     | IsLambda (name,c1,c2) ->
-        let var = make_typed c1 (sort_of env c1) in
-          mkProd (name, c1, type_of (push_rel_assum (name,var) env) c2)
+          mkProd (name, c1, type_of (push_rel_assum (name,c1) env) c2)
     | IsLetIn (name,b,c1,c2) ->
-        let var = make_typed c1 (sort_of env c1) in
-         subst1 b (type_of (push_rel_def (name,b,var) env) c2)
+         subst1 b (type_of (push_rel_def (name,b,c1) env) c2)
     | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
     | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
     | IsApp(f,args)->
@@ -83,8 +81,7 @@ and sort_of env t =
     | IsSort (Prop c) -> type_0
     | IsSort (Type u) -> Type Univ.dummy_univ
     | IsProd (name,t,c2) ->
-        let var = make_typed t (sort_of env t) in
-        (match (sort_of (push_rel_assum (name,var) env) c2) with
+        (match (sort_of (push_rel_assum (name,t) env) c2) with
 	  | Prop _ as s -> s
 	  | Type u2 -> Type Univ.dummy_univ)
     | IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
@@ -99,10 +96,8 @@ let get_sort_of env sigma t = snd (typeur sigma []) env t
 let get_type_of_with_meta env sigma metamap = fst (typeur sigma metamap) env
 
 (* Makes an assumption from a constr *)
-let get_assumption_of env evc c = make_typed_lazy c (get_sort_of env evc)
+let get_assumption_of env evc c = c
 
 (* Makes an unsafe judgment from a constr *)
-let get_judgment_of env evc c =
-  let typ = get_type_of env evc c in
-  { uj_val = c; uj_type = get_assumption_of env evc typ }
+let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
 
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 379a03956..4d472c19c 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -21,7 +21,7 @@ val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
 val get_sort_of : env -> 'a evar_map -> constr -> sorts
 
 (* Makes an assumption from a constr *)
-val get_assumption_of : env -> 'a evar_map -> constr -> typed_type
+val get_assumption_of : env -> 'a evar_map -> constr -> types
 
 (* Makes an unsafe judgment from a constr *)
 val get_judgment_of : env -> 'a evar_map -> constr -> unsafe_judgment
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c1fa26c5f..3d58b6a24 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -625,12 +625,8 @@ let reduce_to_mind env sigma t =
 	     elimrec t' l
            with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
                [< 'sTR"Not an inductive product." >])
-      | IsProd (n,ty,t') ->
-	let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
-	elimrec t' ((n,None,ty')::l)
-      | IsLetIn (n,b,ty,t') ->
-	  let ty' = Retyping.get_assumption_of (Global.env()) Evd.empty ty in
-	  elimrec t' ((n,Some b,ty')::l)
+      | IsProd (n,ty,t') -> elimrec t' ((n,None,ty)::l)
+      | IsLetIn (n,b,ty,t') -> elimrec t' ((n,Some b,ty)::l)
       | _ -> error "Not an inductive product"
  in
  elimrec t []
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index ebab35c2c..23028cc62 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -11,7 +11,7 @@ open Type_errors
 open Typeops
 
 let vect_lift = Array.mapi lift
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
 type 'a mach_flags = {
   fix : bool;
@@ -94,8 +94,7 @@ let rec execute mf env sigma cstr =
     | IsProd (name,c1,c2) ->
         let j = execute mf env sigma c1 in
         let varj = type_judgment env sigma j in
-	let var = assumption_of_type_judgment varj in
-	let env1 = push_rel_assum (name,var) env in
+	let env1 = push_rel_assum (name,varj.utj_val) env in
         let j' = execute mf env1 sigma c2 in
 	let (j,_) = gen_rel env1 sigma name varj j' in
 	j
@@ -103,15 +102,18 @@ let rec execute mf env sigma cstr =
      | IsLetIn (name,c1,c2,c3) ->
         let j1 = execute mf env sigma c1 in
         let j2 = execute mf env sigma c2 in
-	let { uj_val = b; uj_type = t } = cast_rel env sigma j1 j2 in
+	let tj2 = assumption_of_judgment env sigma j2 in
+	let { uj_val = b; uj_type = t },_ = cast_rel env sigma j1 tj2 in
         let j3 = execute mf (push_rel_def (name,b,t) env) sigma c3 in
-	{ uj_val = mkLetIn (name, j1.uj_val, j2.uj_val, j3.uj_val) ;
-	  uj_type = typed_app (subst1 j1.uj_val) j3.uj_type }
+	{ uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ;
+	  uj_type = type_app (subst1 j1.uj_val) j3.uj_type }
   
     | IsCast (c,t) ->
         let cj = execute mf env sigma c in
         let tj = execute mf env sigma t in
-        cast_rel env sigma cj tj
+	let tj = assumption_of_judgment env sigma tj in
+        let j, _ = cast_rel env sigma cj tj in
+	j
 	  
     | IsXtra _ -> anomaly "Typing: found an Extra"
 	  
@@ -123,7 +125,7 @@ and execute_fix mf env sigma lar lfi vdef =
   let env1 = 
     List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in
   let vdefj = execute_array mf env1 sigma vdef in
-  let vdefv = Array.map j_val_only vdefj in
+  let vdefv = Array.map j_val vdefj in
   let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
   (lara,vdefv)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index ee68e518f..eaad2791f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -14,7 +14,7 @@ val unsafe_machine : env -> 'a evar_map -> constr -> unsafe_judgment
 
 val type_of : env -> 'a evar_map -> constr -> constr
 
-val execute_type : env -> 'a evar_map -> constr -> typed_type
+val execute_type : env -> 'a evar_map -> constr -> types
 
-val execute_rec_type : env -> 'a evar_map -> constr -> typed_type
+val execute_rec_type : env -> 'a evar_map -> constr -> types
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 353fe5198..aaf9637f8 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -80,7 +80,7 @@ val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
 (* Exported for program.ml only *)
 val clenv_add_sign : 
-  (identifier * typed_type) -> wc clausenv -> wc clausenv
+  (identifier * types) -> wc clausenv -> wc clausenv
 val constrain_clenv_to_subterm : 
   wc clausenv -> constr * constr -> wc clausenv * constr
 val clenv_constrain_dep_args_of : 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index b1c4a5a2c..ac6bc0630 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -41,7 +41,7 @@ val w_Underlying : walking_constraints -> enamed_declarations
 val w_env        : walking_constraints -> env
 val w_hyps       : walking_constraints -> named_context
 val w_type_of    : walking_constraints -> constr -> constr
-val w_add_sign   : (identifier * typed_type) -> walking_constraints 
+val w_add_sign   : (identifier * types) -> walking_constraints 
                      -> walking_constraints
 
 val w_IDTAC      : w_tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 61126b262..2bf95aed1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -255,7 +255,7 @@ let convert_hyp env sigma id ty =
     (fun env (idc,c,ct) _ ->
        if !check && not (is_conv env sigma ty (body_of_type ct)) then
 	 error "convert-hyp rule passed non-converting term";
-       push_named_decl (idc,c,get_assumption_of env sigma ty) env)
+       push_named_decl (idc,c,ty) env)
 
 let replace_hyp env id d =
   apply_to_hyp env id
@@ -291,16 +291,14 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma c1
-	       and v = mkVar id in
-	       let sg = mk_goal info (push_named_assum (id,a) env) (subst1 v b) in
+	       let sg = mk_goal info (push_named_assum (id,c1) env)
+			  (subst1 (mkVar id) b) in
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma t1
-	       and v = mkVar id in
 	       let sg =
-		 mk_goal info (push_named_def (id,c1,a) env) (subst1 v b) in
+		 mk_goal info (push_named_def (id,c1,t1) env)
+		   (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
 	       if !check then raise (RefinerError IntroNeedsProduct)
@@ -312,17 +310,13 @@ let prim_refiner r sigma goal =
         (match kind_of_term (strip_outer_cast cl) with
 	   | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma c1
-	       and v = mkVar id in
-	       let env' = insert_after_hyp env whereid (id,None,a) in
-	       let sg = mk_goal info env' (subst1 v b) in 
+	       let env' = insert_after_hyp env whereid (id,None,c1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma t1
-	       and v = mkVar id in
-	       let env' = insert_after_hyp env whereid (id,Some c1,a) in
-	       let sg = mk_goal info env' (subst1 v b) in 
+	       let env' = insert_after_hyp env whereid (id,Some c1,t1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in 
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -332,17 +326,13 @@ let prim_refiner r sigma goal =
 	(match kind_of_term (strip_outer_cast cl) with
            | IsProd (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma c1
-	       and v = mkVar id in
-	       let env' = replace_hyp env id (id,None,a) in
-	       let sg = mk_goal info env' (subst1 v b) in
+	       let env' = replace_hyp env id (id,None,c1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in
 	       [sg]
            | IsLetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = get_assumption_of env sigma t1
-	       and v = mkVar id in
-	       let env' = replace_hyp env id (id,Some c1,a) in
-	       let sg = mk_goal info env' (subst1 v b) in
+	       let env' = replace_hyp env id (id,Some c1,t1) in
+	       let sg = mk_goal info env' (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
 	       if !check then error "Introduction needs a product"
@@ -365,8 +355,7 @@ let prim_refiner r sigma goal =
      	check_ind n cl;
 	if !check && mem_named_context f sign then
 	  error ("The name "^(string_of_id f)^" is already used");
-        let a = get_assumption_of env sigma cl in
-        let sg = mk_goal info (push_named_assum (f,a) env) cl in
+        let sg = mk_goal info (push_named_assum (f,cl) env) cl in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
@@ -392,8 +381,7 @@ let prim_refiner r sigma goal =
 		       "mutual inductive declaration");
 	      if mem_named_context f sign then 
 		error "name already used in the environment";
-	      let a = get_assumption_of env sigma ar in
-	      mk_sign (add_named_assum (f,a) sign) (lar',lf',ln')
+	      mk_sign (add_named_assum (f,ar) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
 	      List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
@@ -419,9 +407,7 @@ let prim_refiner r sigma goal =
                 (let _ = lookup_named f env in
                 error "name already used in the environment")
               with
-              |	Not_found ->
-  	        let a = get_assumption_of env sigma ar in
-	        mk_env (push_named_assum (f,a) env) (lar',lf'))
+              |	Not_found -> mk_env (push_named_assum (f,ar) env) (lar',lf'))
 	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 868e71f85..495a9ca82 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -255,9 +255,8 @@ let extract_open_proof sigma pf =
 	       mkNamedProd_or_LetIn (id,c,ty) concl)
             sorted_rels goal.evar_concl
 	in
-	let ass = Retyping.get_assumption_of goal.evar_env sigma abs_concl in
 	let mv = new_meta() in
-	open_obligations := (mv,ass):: !open_obligations;
+	open_obligations := (mv,abs_concl):: !open_obligations;
 	applist (mkMeta mv, List.map (fun (n,_) -> mkRel n) sorted_rels) 
 	  
     | _ -> anomaly "Bug : a case has been forgotten in proof_extractor"
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 4c1e2f977..47d44a9f1 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -117,7 +117,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate
 val weak_undo_pftreestate : pftreestate -> pftreestate
 
 val mk_pftreestate : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
+val extract_open_pftreestate : pftreestate -> constr * (int * types) list
 val extract_pftreestate : pftreestate -> constr
 val first_unproven : pftreestate -> pftreestate
 val last_unproven : pftreestate -> pftreestate
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 8eb0b39e6..717c5212f 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -98,7 +98,7 @@ val weak_undo_pftreestate   : pftreestate -> pftreestate
 val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
 val solve_pftreestate       : tactic -> pftreestate -> pftreestate
 val mk_pftreestate          : goal -> pftreestate
-val extract_open_pftreestate : pftreestate -> constr * (int * typed_type) list
+val extract_open_pftreestate : pftreestate -> constr * (int * types) list
 val extract_pftreestate     : pftreestate -> constr
 val first_unproven          : pftreestate -> pftreestate
 val last_unproven           : pftreestate -> pftreestate
@@ -197,7 +197,7 @@ val w_Underlying        : walking_constraints -> enamed_declarations
 val w_env               : walking_constraints -> env
 val w_hyps              : walking_constraints -> named_context
 val w_type_of           : walking_constraints -> constr -> constr
-val w_add_sign          : (identifier * typed_type) 
+val w_add_sign          : (identifier * types) 
                           -> walking_constraints -> walking_constraints
 val w_IDTAC             : w_tactic
 val w_ORELSE            : w_tactic -> w_tactic -> w_tactic
diff --git a/tactics/auto.ml b/tactics/auto.ml
index c8c75cd5e..3e26eb9a7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -905,9 +905,7 @@ let rec super_search n db_list local_db argl goal =
 let search_superauto n ids argl g = 
   let sigma =
     List.fold_right
-      (fun id -> add_named_assum
-	   (id,Retyping.get_assumption_of (pf_env g) (project g) 
-	      (pf_type_of g (pf_global g id))))
+      (fun id -> add_named_assum (id, pf_type_of g (pf_global g id)))
       ids empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
   let db = Hint_db.add_list db0 (make_local_hint_db g) in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9efdd718e..74f7bf2f2 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -128,13 +128,11 @@ let rec add_prods_sign env sigma t =
     | IsProd (na,c1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-	let j = Retyping.get_assumption_of env sigma c1 in
-        add_prods_sign (Environ.push_named_assum (id,j) env) sigma b'
+        add_prods_sign (Environ.push_named_assum (id,c1) env) sigma b'
     | IsLetIn (na,c1,t1,b) ->
 	let id = Environ.id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
-	let j = Retyping.get_assumption_of env sigma t1 in
-        add_prods_sign (Environ.push_named_def (id,c1,j) env) sigma b'
+        add_prods_sign (Environ.push_named_def (id,c1,t1) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates wether the inversion lemma is dependent or not.
@@ -176,8 +174,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_betadeltaiota env sigma pty in
-  let nptyj = make_typed npty (Retyping.get_sort_of env sigma npty) in
-  let extenv = push_named_assum (p,nptyj) env in
+  let extenv = push_named_assum (p,npty) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
diff --git a/tactics/refine.ml b/tactics/refine.ml
index faa49b3e2..904ed3038 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -138,8 +138,7 @@ let rec compute_metamap env c = match kind_of_term c with
    *    où x est une variable FRAICHE *)
   | IsLambda (name,c1,c2) ->
       let v = fresh env name in
-      let tj = Retyping.get_assumption_of env Evd.empty c1 in
-      let env' = push_named_assum (v,tj) env in
+      let env' = push_named_assum (v,c1) env in
       begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
@@ -179,9 +178,7 @@ let rec compute_metamap env c = match kind_of_term c with
   | IsFix ((ni,i),(ai,fi,v)) ->
       let vi = List.rev (List.map (fresh env) fi) in
       let env' =
-	List.fold_left
-	  (fun env (v,ar) -> push_named_assum (v,Retyping.get_assumption_of env Evd.empty ar) env)
-	  env
+	List.fold_left (fun env (v,ar) -> push_named_assum (v, ar) env) env
 	  (List.combine vi (Array.to_list ai)) 
       in
       let a = Array.map
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 6f7499057..2a6ddcbac 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -1717,9 +1717,9 @@ let rec lisvarprop = function
 let rec constr_lseq gls = function
   | [] -> []
   | (idx,c,hx)::rest -> 
-      match Retyping.get_sort_of (pf_env gls) (project gls) (incast_type hx) with
+      match Retyping.get_sort_of (pf_env gls) (project gls) hx with
         | Prop Null -> 
-            (TVar(string_of_id idx),tauto_of_cci_fmla gls (body_of_type hx))
+            (TVar(string_of_id idx),tauto_of_cci_fmla gls hx)
             :: constr_lseq gls rest
         |_-> constr_lseq gls rest
 
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 4943756e3..ab046025f 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -93,9 +93,9 @@ let clenv_constrain_with_bindings bl clause =
 let add_prod_rel sigma (t,env) =
   match kind_of_term t with
     | IsProd (na,t1,b) ->
-        (b,push_rel_assum (na,Retyping.get_assumption_of env sigma t1) env)
+        (b,push_rel_assum (na, t1) env)
     | IsLetIn (na,c1,t1,b) ->
-        (b,push_rel_def (na,c1,Retyping.get_assumption_of env sigma t1) env)
+        (b,push_rel_def (na,c1, t1) env)
     | _ -> failwith "add_prod_rel"
 
 let rec add_prods_rel sigma (t,env) =
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index af96177b3..b3d372f21 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -33,10 +33,10 @@ val add_prods_rel : 'a evar_map -> constr * env -> constr * env
 
 (*i**
 val add_prod_sign : 
-  'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+  'a evar_map -> constr * types signature -> constr * types signature
 
 val add_prods_sign : 
-  'a evar_map -> constr * typed_type signature -> constr * typed_type signature
+  'a evar_map -> constr * types signature -> constr * types signature
 **i*)
 
 val res_pf_THEN : 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6150f0c02..6d8264d9c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -140,7 +140,7 @@ let build_mutual lparams lnamearconstrs finite =
 	(fun (env,arl) (recname,arityc,_) -> 
            let raw_arity = mkProdCit lparams arityc in
            let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
-	   let arity = Typeops.assumption_of_type_judgment arj in
+	   let arity = arj.utj_val in
 	   let env' = Environ.push_rel_assum (Name recname,arity) env in
 	   (env', (arity::arl)))
 	(env0,[]) lnamearconstrs 
@@ -215,7 +215,7 @@ let build_recursive lnameargsardef =
         (fun (env,arl) (recname,lparams,arityc,_) -> 
            let raw_arity = mkProdCit lparams arityc in
            let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
-	   let arity = Typeops.assumption_of_type_judgment arj in
+	   let arity = arj.utj_val in
            declare_variable recname
 	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
@@ -239,7 +239,7 @@ let build_recursive lnameargsardef =
   if lnamerec <> [] then begin
     let recvec = 
       Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
-    let varrec = Array.of_list (List.map incast_type larrec) in
+    let varrec = Array.of_list larrec in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
@@ -283,7 +283,7 @@ let build_corecursive lnameardef =
       List.fold_left 
         (fun (env,arl) (recname,arityc,_) -> 
            let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
-	   let arity = Typeops.assumption_of_type_judgment arj in
+	   let arity = arj.utj_val in
            declare_variable recname
 	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
@@ -310,7 +310,7 @@ let build_corecursive lnameardef =
 	[||] 
       else 
 	Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
-    let varrec = Array.of_list (List.map incast_type larrec) in
+    let varrec = Array.of_list larrec in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 2cfd2ca64..f25861d88 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -26,8 +26,6 @@ let recalc_sp sp =
 
 let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
 
-let generalize_type = generalize_without_universes
-
 type modification_action = ABSTRACT | ERASE
 
 let interp_modif absfun oper (oper',modif) cl = 
@@ -129,11 +127,9 @@ let abstract_inductive ids_to_abs hyps inds =
     let inds' =
       List.map
       	(function (tname,arity,cnames,lc) -> 
-	   let arity' = generalize_type d arity in
+	   let arity' = mkNamedProd_or_LetIn d arity in
 	   let lc' =
-	     List.map
-	       (fun b -> generalize_type d (typed_app (substl new_refs) b))
-	       lc
+	     List.map (fun b -> mkNamedProd_or_LetIn d (substl new_refs b)) lc
 	   in
            (tname,arity',cnames,lc'))
       	inds
@@ -171,7 +167,7 @@ let abstract_constant ids_to_abs hyps (body,typ) =
 	| Some { contents = Recipe f } ->
 	    Some (ref (Recipe (fun () -> mkNamedLambda_or_LetIn decl (f()))))
       in
-      let typ' = generalize_type decl typ in
+      let typ' = mkNamedProd_or_LetIn decl typ in
       (rest, body', typ', ABSTRACT::modl)
   in
   let (_,body',typ',revmodl) =
@@ -206,8 +202,8 @@ let expmod_constr oldenv modlist c =
     | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
     | _ -> simpfun c'
 
-let expmod_type oldenv modlist c = 
-  typed_app (expmod_constr oldenv modlist) c
+let expmod_type oldenv modlist c =
+  type_app (expmod_constr oldenv modlist) c
 
 let expmod_constant_value opaque oldenv modlist = function
   | None -> None
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index 0ba0e73a7..5680af6f5 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -51,7 +51,7 @@ val explain_ill_formed_branch :
   path_kind -> env -> constr -> int -> constr -> constr -> std_ppcmds
 
 val explain_generalization :
-  path_kind -> env -> name * typed_type -> constr -> std_ppcmds
+  path_kind -> env -> name * types -> constr -> std_ppcmds
 
 val explain_actual_type :
   path_kind -> env -> constr -> constr -> constr -> std_ppcmds
@@ -62,6 +62,6 @@ val explain_ill_formed_rec_body :
 
 val explain_ill_typed_rec_body  :
   path_kind -> env -> int -> name list -> unsafe_judgment array 
-    -> typed_type array -> std_ppcmds
+    -> types array -> std_ppcmds
 
 end
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 321f9bf31..38d9e670d 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -66,22 +66,22 @@ let all_vars t =
 let print_id_list l = 
   [< 'sTR "[" ; prlist_with_sep pr_coma print_id l; 'sTR "]" >]
 
+open Environ
+
 let typecheck_params_and_field ps fs =
   let env0 = Global.env () in
   let env1,newps =
     List.fold_left
       (fun (env,newps) (id,t) -> 
-         let tj = type_judgment_of_rawconstr Evd.empty env t in
-	 let ass = Typeops.assumption_of_type_judgment tj in
-         (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newps))
+         let tj = interp_type Evd.empty env t in
+         (push_named_assum (id,tj) env,(id,tj)::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) (id,t) -> 
-         let tj = type_judgment_of_rawconstr Evd.empty env t in
-	 let ass = Typeops.assumption_of_type_judgment tj in
-         (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs
+         let ass = interp_type Evd.empty env t in
+         (push_named_assum (id,ass) env,(id,ass)::newfs)) (env1,[]) fs
   in
   List.rev(newps),List.rev(newfs)