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

22 files changed, 209 insertions, 265 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