Mise en place d'un choix constr/typed_type en remplacement de certains Cast

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

16 files changed, 130 insertions, 115 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d97bb916bb..a48384389d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -47,7 +47,7 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_lc : constr array;
+  mind_lc : typed_type array;
   mind_arity : typed_type;
   mind_sort : sorts;
   mind_nrealargs : int;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d05c07f14b..eab3cb0e48 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -53,7 +53,7 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_lc : constr array;
+  mind_lc : typed_type array;
   mind_arity : typed_type;
   mind_sort : sorts;
   mind_nrealargs : int;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4f9d4e957e..73a8c6487e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -297,9 +297,8 @@ let import cenv env =
 
 type unsafe_judgment = { 
   uj_val : constr;
-  uj_type : constr;
-  uj_kind : constr }
+  uj_type : typed_type }
 
-let cast_of_judgment = function
-  | { uj_val = DOP2 (Cast,_,_) as c } -> c
-  | { uj_val = c; uj_type = ty } -> mkCast c ty
+type unsafe_type_judgment = { 
+  utj_val : constr;
+  utj_type : sorts }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8f73b9779b..c8e3642be8 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -96,7 +96,8 @@ val import : compiled_env -> env -> env
 
 type unsafe_judgment = { 
   uj_val : constr;
-  uj_type : constr;
-  uj_kind : constr }
+  uj_type : typed_type }
 
-val cast_of_judgment : unsafe_judgment -> constr
+type unsafe_type_judgment = { 
+  utj_val : constr;
+  utj_type : sorts }
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5cedd542c5..979d24536a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -293,6 +293,7 @@ let listrec_mconstr env ntypes nparams i indlc =
   let lna = it_dbenv (fun l na t -> na::l) [] (context env) in
   Array.map
     (fun c ->
+       let c = body_of_type c in
        try
 	 check_construct true (1+nparams) (decomp_par nparams c)
        with IllFormedInd err -> 
@@ -330,7 +331,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
       (fun acc (_,ar,_,_,_,lc) -> 
 	 Idset.union (global_vars_set (body_of_type ar))
 	   (Array.fold_left
-	      (fun acc c -> Idset.union (global_vars_set c) acc)
+	      (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc)
 	      acc
 	      lc))
       Idset.empty inds
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index c35459454c..5a7f040d94 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 * constr array)
+   (identifier * typed_type * identifier list * bool * bool * typed_type array)
       list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 85ea816e64..80b60f2ad2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -35,12 +35,14 @@ let mis_typepath mis =
 let mis_consnames mis = mis.mis_mip.mind_consnames
 let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
 
-let mis_lc mis =
+let mis_typed_lc mis =
   let ids = ids_of_sign mis.mis_mib.mind_hyps in
   let args = Array.to_list mis.mis_args in
-  Array.map (fun t -> Instantiate.instantiate_constr ids t args)
+  Array.map (fun t -> Instantiate.instantiate_type ids t args)
     mis.mis_mip.mind_lc
 
+let mis_lc mis = Array.map body_of_type (mis_typed_lc mis)
+
 (* gives the vector of constructors and of 
    types of constructors of an inductive definition 
    correctly instanciated *)
@@ -57,12 +59,12 @@ let mis_type_mconstructs mispec =
    Array.map (substl (list_tabulate make_Ik ntypes)) specif)
 
 let mis_type_mconstruct i mispec =
-  let specif = mis_lc mispec
+  let specif = mis_typed_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
   let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
   if i > nconstr then error "Not enough constructors in the type";
-  substl (list_tabulate make_Ik ntypes) specif.(i-1)
+  typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
 
 let mis_typed_arity mis =
   let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index fa989110cb..936c9093ae 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -45,7 +45,7 @@ val mis_inductive : inductive_instance -> inductive
 val mis_arity : inductive_instance -> constr
 val mis_lc : inductive_instance -> constr array
 val mis_type_mconstructs : inductive_instance -> constr array * constr array
-val mis_type_mconstruct : int -> inductive_instance -> constr
+val mis_type_mconstruct : int -> inductive_instance -> typed_type
 val mis_params_ctxt : inductive_instance -> (name * constr) list
 val mis_sort : inductive_instance -> sorts
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 85a335ee8e..88e42fc864 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1191,11 +1191,12 @@ let is_type_arity env sigma =
   srec 
 
 let is_info_type env sigma t =
-  let s = level_of_type t in
+  let s = t.utj_type in
   (s = Prop Pos) ||
   (s <> Prop Null && 
-   try info_arity env sigma (body_of_type t) with IsType -> true)
+   try info_arity env sigma t.utj_val with IsType -> true)
 
+(* Pour l'extraction 
 let is_info_cast_type env sigma c = 
   match c with  
     | DOP2(Cast,c,t) -> 
@@ -1205,6 +1206,7 @@ let is_info_cast_type env sigma c =
 	   
 let contents_of_cast_type env sigma c = 
   if is_info_cast_type env sigma c then Pos else Null
+*)
 
 let is_info_sort = is_info_arity
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 9be27fb7cc..0d2c39c5f5 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -115,9 +115,11 @@ val is_info_arity : env -> 'a evar_map -> constr -> bool
 val is_info_sort : env -> 'a evar_map -> constr -> bool
 val is_logic_arity : env -> 'a evar_map -> constr -> bool
 val is_type_arity : env -> 'a evar_map -> constr -> bool
-val is_info_type : env -> 'a evar_map -> typed_type -> bool
+val is_info_type : env -> 'a evar_map -> unsafe_type_judgment -> bool
+(*i Pour l'extraction
 val is_info_cast_type : env -> 'a evar_map -> constr -> bool
 val contents_of_cast_type : env -> 'a evar_map -> constr -> contents
+i*)
 val poly_args : env -> 'a evar_map -> constr -> int list
 
 val whd_programs : 'a reduction_function
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 19bf52c84e..231aea23ad 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -19,8 +19,7 @@ open Indtypes
 type judgment = unsafe_judgment
 
 let j_val j = j.uj_val
-let j_type j = j.uj_type
-let j_kind j = j.uj_kind
+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)
@@ -68,8 +67,7 @@ let rec execute mf env cstr =
 	(make_judge cstr (type_of_inductive env Evd.empty ind), cst0)
 	  
     | IsMutConstruct c -> 
-	let (typ,kind) =destCast (type_of_constructor env Evd.empty c) in
-        ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
+	(make_judge cstr (type_of_constructor env Evd.empty c), cst0)
 	  
     | IsMutCase (ci,p,c,lf) ->
         let (cj,cst1) = execute mf env c in
@@ -118,10 +116,11 @@ let rec execute mf env cstr =
 	  
      | IsProd (name,c1,c2) ->
         let (j,cst1) = execute mf env c1 in
-        let var = assumption_of_judgment env Evd.empty j in
+        let varj = type_judgment env Evd.empty j in
+	let var = assumption_of_type_judgment varj in
 	let env1 = push_rel (name,var) env in
         let (j',cst2) = execute mf env1 c2 in
-	let (j,cst3) = gen_rel env1 Evd.empty name var j' in
+	let (j,cst3) = gen_rel env1 Evd.empty name varj j' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
 	(j, cst)
 	  
@@ -158,12 +157,11 @@ and execute_list mf env = function
       let (jr,cst2) = execute_list mf env r in
       (j::jr, Constraint.union cst1 cst2)
 
-
 (* The typed type of a judgment. *)
 
 let execute_type mf env constr = 
   let (j,cst) = execute mf env constr in
-  (assumption_of_judgment env Evd.empty j, cst)
+  (type_judgment env Evd.empty j, cst)
 
 
 (* Exported machines.  First safe machines, with no general fixpoint
@@ -202,7 +200,7 @@ let unsafe_machine_type env constr =
 (* ``Type of'' machines. *)
 
 let type_of env c = 
-  let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type
+  let (j,_) = safe_machine env c in nf_betaiota env Evd.empty (body_of_type j.uj_type)
 
 (* obsolètes
 let type_of_type env c = 
@@ -280,12 +278,12 @@ let add_constant_with_value sp body typ env =
 	  let (jt,cst') = safe_machine env ty in
 	  let env'' = add_constraints cst' env' in
 	  try
-	    let cst'' = conv env'' Evd.empty jb.uj_type jt.uj_val in
+	    let cst'' = conv env'' Evd.empty (body_of_type jb.uj_type) jt.uj_val in
 	    let env'' = add_constraints cst'' env'' in
 	    (env'', assumption_of_judgment env'' Evd.empty jt, 
 	     Constraint.union cst' cst'')
 	  with NotConvertible -> 
-	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+	    error_actual_type CCI env jb.uj_val (body_of_type jb.uj_type) jt.uj_val
   in
   let ids = 
     Idset.union (global_vars_set body) (global_vars_set (body_of_type ty))
@@ -353,12 +351,13 @@ let max_universe (s1,cst1) (s2,cst2) g =
 let rec infos_and_sort env t =
   match kind_of_term t with
     | IsProd (name,c1,c2) ->
-        let (var,cst1) = safe_machine_type env c1 in
+        let (varj,cst1) = safe_machine_type env c1 in
+	let var = assumption_of_type_judgment varj in
 	let env1 = Environ.push_rel (name,var) env in
 	let (infos,smax,cst) = infos_and_sort env1 c2 in
-	let s1 = level_of_type var in
+	let s1 = varj.utj_type in
 	let smax',cst' = max_universe (s1,cst1) (smax,cst) (universes env) in
-	let logic = not (is_info_type env Evd.empty var) in
+	let logic = not (is_info_type env Evd.empty varj) in
 	let small = is_small s1 in
 	((logic,small) :: infos, smax', cst')
     | IsCast (c,t) -> infos_and_sort env c
@@ -400,7 +399,7 @@ let type_one_constructor env_ar nparams arsort c =
   let (j,cst2) = safe_machine_type env_ar c in
   (*C'est idiot, cst1 et cst2 sont essentiellement des copies l'un de l'autre*)
   let cst3 =enforce_type_constructor arsort max (Constraint.union cst1 cst2) in
-  (infos, j, cst3)
+  (infos, assumption_of_type_judgment j, cst3)
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
   let arsort = sort_of_arity env_ar ar in
@@ -412,7 +411,7 @@ let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
       vc
       ([],[],Constraint.empty)
   in
-  let vc' = Array.of_list (List.map incast_type jlc) in
+  let vc' = Array.of_list jlc in
   let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
   let (_,tyar) = lookup_rel (ninds+1-i) env_ar in
   ((id,tyar,cnames,issmall,isunit,vc'), cst')
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 07857dea96..4ed912d4cf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -53,13 +53,12 @@ val import : compiled_env -> safe_environment -> safe_environment
 
 val env_of_safe_env : safe_environment -> env
 
+(*i For debug
 (*s Typing without information. *)
-
 type judgment
 
 val j_val : judgment -> constr
 val j_type : judgment -> constr
-val j_kind : judgment -> constr
 
 val safe_machine : safe_environment -> constr -> judgment * constraints
 val safe_machine_type : safe_environment -> constr -> typed_type * constraints
@@ -81,5 +80,5 @@ i*)
 (*s Typing with information (extraction). *)
 
 type information = Logic | Inf of judgment
-
+i*)
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 6b8e094b9a..e97a2b2193 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -68,7 +68,7 @@ type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
 
-(**)
+(*
 type typed_type = sorts judge
 type typed_term = typed_type judge
 
@@ -84,8 +84,10 @@ let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
 let outcast_type = function
    DOP2 (Cast, b, DOP0 (Sort s)) -> {body=b; typ=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
 type typed_term = typed_type judge
 
@@ -98,7 +100,8 @@ 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
+(**)
 
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
@@ -1481,14 +1484,14 @@ module Htype =
     struct
       type t = typed_type
       type u = (constr -> constr) * (sorts -> sorts)
-(**)
+(*
       let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ}
       let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ
+*)
 (**)
-(*
       let hash_sub (hc,hs) j = hc j
       let equal j1 j2 = j1==j2
-*)
+(**)
       let hash = Hashtbl.hash
     end)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index cc5a8954d0..787f51c63b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -65,6 +65,8 @@ type typed_term = typed_type judge
 val make_typed : constr -> sorts -> typed_type
 
 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 body_of_type : typed_type -> constr
 val level_of_type : typed_type -> sorts
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index e227111d0d..0a53f6b770 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -17,34 +17,36 @@ open Type_errors
 
 let make_judge v tj =
   { uj_val = v;
-    uj_type = body_of_type tj;
-    uj_kind= DOP0 (Sort (level_of_type tj)) }
+    uj_type = tj }
 
 let j_val_only j = j.uj_val
 (* Faut-il caster ? *)
 let j_val = j_val_only
 
-let j_val_cast j = mkCast j.uj_val j.uj_type
-
-let typed_type_of_judgment env sigma j =
-  match whd_betadeltaiota env sigma j.uj_kind with
-    | DOP0(Sort s) -> make_typed j.uj_type s
-    | _ -> error_not_type CCI env j.uj_type
+let j_val_cast j = mkCast j.uj_val (body_of_type j.uj_type)
 
+let typed_type_of_judgment env sigma j = j.uj_type
 
 let assumption_of_judgment env sigma j =
-  match whd_betadeltaiota env sigma j.uj_type with
+  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
     | DOP0(Sort s) -> make_typed j.uj_val s
     | _ -> error_assumption CCI env j.uj_val
 
+let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
+
+let type_judgment env sigma j =
+  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
+    | DOP0(Sort s) -> {utj_val = j.uj_val; utj_type = s }
+    | _ -> error_assumption CCI env j.uj_val
+
+
 (* Type of a de Bruijn index. *)
 	  
 let relative env n = 
   try
     let (_,typ) = lookup_rel n env in
     { uj_val  = Rel n;
-      uj_type = lift n (body_of_type typ);
-      uj_kind = DOP0 (Sort (level_of_type typ)) }
+      uj_type = typed_app (lift n) typ }
   with Not_found -> 
     error_unbound_rel CCI env n
 
@@ -99,8 +101,10 @@ let type_of_inductive env sigma i =
 
 (* Constructors. *)
 
+(*
 let type_mconstructs env sigma mind =
   mis_type_mconstructs (lookup_mind_specif mind env)
+*)
 
 let type_mconstruct env sigma i mind =
   mis_type_mconstruct i (lookup_mind_specif mind env)
@@ -110,10 +114,6 @@ let type_of_constructor env sigma cstr =
     (index_of_constructor cstr)
     (inductive_of_constructor cstr)
 
-let type_inst_construct i (IndFamily (mis,globargs)) =
-  let tc = mis_type_mconstruct i mis in
-  prod_applist tc globargs
-
 let type_of_existential env sigma c =
   Instantiate.existential_type sigma (destEvar c)
 
@@ -121,7 +121,7 @@ let type_of_existential env sigma c =
 
 let rec mysort_of_arity env sigma c =
   match whd_betadeltaiota env sigma c with
-    | DOP0(Sort( _)) as c' -> c'
+    | DOP0(Sort(s)) -> s
     | DOP2(Prod,_,DLAM(_,c2)) -> mysort_of_arity env sigma c2
     | _ -> invalid_arg "mysort_of_arity"
 
@@ -209,29 +209,27 @@ let check_branches_message env sigma (c,ct) (explft,lft) =
   done
 
 let type_of_case env sigma ci pj cj lfj =
-  let lft = Array.map (fun j -> j.uj_type) lfj in
+  let lft = Array.map (fun j -> body_of_type j.uj_type) lfj in
   let indspec =
-    try find_inductive env sigma cj.uj_type
-    with Induc -> error_case_not_inductive CCI env cj.uj_val cj.uj_type in
+    try find_inductive env sigma (body_of_type cj.uj_type)
+    with Induc ->
+      error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in
   let (bty,rslty) =
-    type_case_branches env sigma indspec pj.uj_type pj.uj_val cj.uj_val in
-  let kind = mysort_of_arity env sigma pj.uj_type in
-  check_branches_message env sigma (cj.uj_val,cj.uj_type) (bty,lft);
+    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  = mkMutCaseA ci (j_val pj) (j_val cj) (Array.map j_val lfj);
-    uj_type = rslty;
-    uj_kind = kind }
+    uj_type = make_typed rslty kind }
 
 (* Prop and Set *)
 
 let judge_of_prop =
   { uj_val = DOP0(Sort prop);
-    uj_type = DOP0(Sort type_0);
-    uj_kind = DOP0(Sort type_1) }
+    uj_type = make_typed (DOP0(Sort type_0)) type_1 }
 
 let judge_of_set =
   { uj_val = DOP0(Sort spec);
-    uj_type = DOP0(Sort type_0);
-    uj_kind = DOP0(Sort type_1) }
+    uj_type = make_typed (DOP0(Sort type_0)) type_1 }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
@@ -242,14 +240,13 @@ let judge_of_prop_contents = function
 let judge_of_type u =
   let (uu,uuu,c) = super_super u in
   { uj_val = DOP0 (Sort (Type u));
-    uj_type = DOP0 (Sort (Type uu));
-    uj_kind = DOP0 (Sort (Type uuu)) },
+    uj_type = make_typed (DOP0(Sort (Type uu))) (Type uuu) },
   c
 
 let type_of_sort c =
   match c with
-    | DOP0 (Sort (Type u)) -> let (uu,cst) = super u in mkType uu, cst
-    | DOP0 (Sort (Prop _)) -> mkType prop_univ, Constraint.empty
+    | DOP0 (Sort (Type u)) -> let (uu,cst) = super u in Type uu, cst
+    | DOP0 (Sort (Prop _)) -> Type prop_univ, Constraint.empty
     | _ -> invalid_arg "type_of_sort"
 
 (* Type of a lambda-abstraction. *)
@@ -273,46 +270,52 @@ let sort_of_product_without_univ domsort rangsort =
            | Prop _ -> rangsort
            | Type u1 -> Type dummy_univ)
 
+let typed_product_without_universes name var c =
+  typed_combine (mkProd name) 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 (mkProd name) hacked_sort_of_product var c, !rcst
+
 let abs_rel env sigma name var j =
-  let rngtyp = whd_betadeltaiota env sigma j.uj_kind in
   let cvar = incast_type var in
-  let (s,cst) =
-    sort_of_product (level_of_type var) (destSort rngtyp) (universes env) in
+  let typ,cst = typed_product env name var j.uj_type in
   { uj_val = mkLambda name cvar (j_val j);
-    uj_type = mkProd name cvar j.uj_type;
-    uj_kind = mkSort s },
+    uj_type = typ },
   cst
 
 (* Type of a product. *)
 
-let gen_rel env sigma name var j =
-  let jtyp = whd_betadeltaiota env sigma j.uj_type in
-  let jkind = whd_betadeltaiota env sigma j.uj_kind in
-  let j = { uj_val = j.uj_val; uj_type = jtyp; uj_kind = jkind } in
-  if isprop jkind then 
-    error "Proof objects can only be abstracted" 
-  else
-    match jtyp with
-      | DOP0(Sort s) ->
-	  let (s',g) = sort_of_product (level_of_type var) 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_val_cast j);
-            uj_type = res_type;
-            uj_kind = res_kind }, g'
-      | _ -> 
+let gen_rel env sigma name varj j =
+  let var = assumption_of_type_judgment varj in
+  match whd_betadeltaiota env sigma (body_of_type j.uj_type) with
+    | DOP0(Sort s) as ts ->
+	let t = mkCast j.uj_val ts in
+	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) t;
+          uj_type = make_typed res_type res_kind },
+	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 (name,var) j.uj_val
 
 (* Type of a cast. *)
 	    
 let cast_rel env sigma cj tj =
-  if is_conv_leq env sigma cj.uj_type tj.uj_val then
+  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.uj_val;
-      uj_kind = whd_betadeltaiota env sigma tj.uj_type }
+      uj_type = tj }
   else 
-    error_actual_type CCI env cj.uj_val cj.uj_type tj.uj_val
+    error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) (body_of_type tj)
 
 (* Type of an application. *)
 
@@ -320,8 +323,7 @@ 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 = typ;
-          uj_kind = funj.uj_kind },
+          uj_type = typed_app (fun _ -> typ) funj.uj_type },
 	cst
     | hj::restjl ->
         match whd_betadeltaiota env sigma typ with
@@ -330,16 +332,16 @@ let apply_rel_list env sigma nocheck argjl funj =
                 apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl
 	      else 
 		(try 
-		   let c = conv_leq env sigma hj.uj_type c1 in
+		   let c = conv_leq env sigma (body_of_type hj.uj_type) c1 in
 		   let cst' = Constraint.union cst c in
 		   apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
 		 with NotConvertible -> 
-		   error_cant_apply_bad_type CCI env (n,hj.uj_type,c1)
+		   error_cant_apply_bad_type CCI env (n,body_of_type hj.uj_type,c1)
 		     funj argjl)
           | _ ->
 	      error_cant_apply_not_functional CCI env funj argjl
   in 
-  apply_rec 1 funj.uj_type Constraint.empty argjl
+  apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl
 
 
 (* Fixpoints. *)
@@ -808,7 +810,7 @@ let type_fixpoint env sigma lna lar vdefj =
 	 try conv_leq env sigma def (lift lt ar) 
 	 with NotConvertible -> raise (IllBranch i))
       env sigma
-      (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
+      (Array.map (fun j -> body_of_type j.uj_type) vdefj) (Array.map body_of_type lar)
   with IllBranch i ->
     error_ill_typed_rec_body CCI env i lna vdefj lar
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3d2074c977..625a33193c 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -25,6 +25,9 @@ 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
+val type_judgment : 
+  env -> 'a evar_map -> unsafe_judgment -> unsafe_type_judgment
 
 val relative : env -> int -> unsafe_judgment
 
@@ -32,7 +35,7 @@ val type_of_constant : env -> 'a evar_map -> constant -> typed_type
 
 val type_of_inductive : env -> 'a evar_map -> inductive -> typed_type
 
-val type_of_constructor : env -> 'a evar_map -> constructor -> constr
+val type_of_constructor : env -> 'a evar_map -> constructor -> typed_type
 
 val type_of_existential : env -> 'a evar_map -> constr -> constr
 
@@ -48,12 +51,15 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 
 val judge_of_type : universe -> unsafe_judgment * constraints
 
+val typed_product_without_universes :
+  name -> typed_type -> typed_type -> typed_type
+
 val abs_rel : 
   env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val gen_rel :
-  env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
+  env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
 val sort_of_product : sorts -> sorts -> universes -> sorts * constraints
@@ -79,9 +85,6 @@ open Inductive
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
 
-(* Returns the type of the [i]$^{th}$ constructor of the inductive family *)
-val type_inst_construct : int -> inductive_family -> constr 
-
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
 
 val keep_hyps : var_context -> Idset.t -> var_context