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

29 files changed, 395 insertions, 289 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 35cd38acb..a67f15e8e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -38,13 +38,10 @@ let prvar ((id,a)) =
     pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ; 
 	  term0 (gLOB nil_sign) a >]
 
-let genprj f j = [< (f (gLOB nil_sign)j.uj_val); 
-                 'sTR " : ";
-               (f (gLOB nil_sign)j.uj_type);
-                  'sTR " : ";
-               (f  (gLOB nil_sign)j.uj_kind)>]
+let genprj f j =
+  let (c,t) = Termast.with_casts f j in [< c; 'sTR " : "; t >]
 
-let prj j = pP (genprj term0 j)
+let prj j = pP (genprj prjudge j)
 
 
 let prsp sp = pP[< 'sTR(string_of_path sp) >]
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d97bb916b..a48384389 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 d05c07f14..eab3cb0e4 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 4f9d4e957..73a8c6487 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 8f73b9779..c8e3642be 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 5cedd542c..979d24536 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 c35459454..5a7f040d9 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 85ea816e6..80b60f2ad 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 fa989110c..936c9093a 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 85a335ee8..88e42fc86 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 9be27fb7c..0d2c39c5f 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 19bf52c84..231aea23a 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 07857dea9..4ed912d4c 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 6b8e094b9..e97a2b219 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 cc5a8954d..787f51c63 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 e227111d0..0a53f6b77 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 3d2074c97..625a33193 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
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 55664cf1e..c7fcbd729 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -44,7 +44,7 @@ let print_closed_sections = ref false
 let print_typed_value_in_env env (trm,typ) =
   let sign = Environ.var_context env in
   [< prterm_env (gLOB sign) trm ; 'fNL ;
-     'sTR "     : "; prterm_env (gLOB sign) typ ; 'fNL >]
+     'sTR "     : "; prtype_env (gLOB sign) typ ; 'fNL >]
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
 
@@ -142,7 +142,9 @@ let print_mutual sp mib =
     let ass_name = assumptions_for_print (lparsname@(Array.to_list lna)) in
     let lidC =
       Array.to_list 
-        (array_map2 (fun id c -> (id,snd (decomp_n_prod env evd nparams c)))
+        (array_map2
+	   (fun id c ->
+	      (id,snd (decomp_n_prod env evd nparams (body_of_type c))))
            mip.mind_consnames lC) in
     let plidC = prlist_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
                   (prass ass_name) lidC in
@@ -332,14 +334,15 @@ let list_filter_vec f vec =
    of the object, the assumptions that will make it possible to print its type,
    and the constr term that represent its type. *)
 
-let print_constructors_head 
+(*
+let print_constructors_head
   (fn : string -> unit assumptions -> constr -> unit) c lna mip = 
   let lC = mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = array_map2 (fun id c_0 -> (id,c_0)) mip.mind_consnames lC in
-  let flid = list_filter_vec (fun (_,c_0) -> head_const c_0 = c) lidC in
+  let flid = list_filter_vec (fun (_,c_0) -> head_const (body_of_type c_0) = c) lidC in
   List.iter
-    (function (id,c_0) -> fn (string_of_id id) ass_name c_0) flid
+    (function (id,c_0) -> fn (string_of_id id) ass_name (body_of_type c_0)) flid
     
 let print_all_constructors_head fn c mib = 
   let mipvec = mib.mind_packets 
@@ -353,8 +356,17 @@ let print_constructors_rel fn lna mip =
   let lC = mip.mind_lc in
   let ass_name = assumptions_for_print lna in
   let lidC = array_map2 (fun id c -> (id,c)) mip.mind_consnames lC in
-  let flid = list_filter_vec (fun (_,c) -> isRel (head_const c)) lidC in
-  List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid
+  let flid = list_filter_vec (fun (_,c) -> isRel (head_const (body_of_type c))) lidC in
+  List.iter (function (id,c) -> fn (string_of_id id) ass_name (body_of_type c))
+    flid
+*)
+
+let print_constructors fn lna mip = 
+  let ass_name = assumptions_for_print lna in
+  let _ =
+    array_map2 (fun id c -> fn (string_of_id id) ass_name (body_of_type c))
+    mip.mind_consnames mip.mind_lc
+  in ()
 
 let crible (fn : string -> unit assumptions -> constr -> unit) name =
   let hyps = gLOB (Global.var_context()) in
@@ -380,9 +392,10 @@ let crible (fn : string -> unit assumptions -> constr -> unit) name =
 		   (fun mip -> Name mip.mind_typename) mib.mind_packets in
                (match const with 
 		  | (DOPN(MutInd(sp',tyi),_)) -> 
-		      if sp = objsp_of sp' then print_constructors_rel fn lna
-			(mind_nth_type_packet mib tyi) 
-		  | _ -> print_all_constructors_head fn const mib); 
+		      if sp = objsp_of sp' then
+			print_constructors fn lna
+			  (mind_nth_type_packet mib tyi)
+		  | _ -> ());
                crible_rec rest
 	   | _ -> crible_rec rest)
 
@@ -420,12 +433,11 @@ let print_val env {uj_val=trm;uj_type=typ} =
   print_typed_value_in_env env (trm,typ)
     
 let print_type env {uj_val=trm;uj_type=typ} =
-  print_typed_value_in_env env (trm, nf_betaiota env Evd.empty typ)
+  print_typed_value_in_env env (trm, typed_app (nf_betaiota env Evd.empty) typ)
     
 let print_eval red_fun env {uj_val=trm;uj_type=typ} =
-  let ntrm = red_fun env Evd.empty trm
-  and ntyp = nf_betaiota env Evd.empty typ in
-  [< 'sTR "     = "; print_typed_value_in_env env (ntrm, ntyp) >]
+  let ntrm = red_fun env Evd.empty trm in
+  [< 'sTR "     = "; print_type env {uj_val = ntrm; uj_type = typ} >]
 
 let print_name name = 
   let str = string_of_id name in 
@@ -471,14 +483,14 @@ let print_opaque_name name =
 	  let cb = Global.lookup_constant sp in
           if is_defined cb then
 	    let typ = constant_type env Evd.empty cst in
-            print_typed_value (constant_value env x, body_of_type typ)
+            print_typed_value (constant_value env x, typ)
           else 
 	    anomaly "print_opaque_name"
       | IsMutInd ((sp,_),_) ->
           print_mutual sp (Global.lookup_mind sp)
       | IsMutConstruct cstr -> 
 	  let ty = Typeops.type_of_constructor env sigma cstr in
-	  print_typed_value(x, ty)
+	  print_typed_value (x, ty)
       | IsVar id ->
           let a = snd(lookup_sign id sign) in 
 	  print_var (string_of_id id) a
@@ -521,7 +533,7 @@ let fprint_var name typ =
   [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >]
 
 let fprint_judge {uj_val=trm;uj_type=typ} = 
-  [< fprterm trm; 'sTR" : " ; fprterm typ >]
+  [< fprterm trm; 'sTR" : " ; fprterm (body_of_type typ) >]
 
 let unfold_head_fconst = 
   let rec unfrec = function
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 5a4f8ae5b..89bbdb2e9 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -95,6 +95,10 @@ let prterm = prterm_env (gLOB nil_sign)
 let prtype_env env typ = prterm_env env (incast_type typ)
 let prtype = prtype_env (gLOB nil_sign)
 
+let prjudge_env env j =
+  (prterm_env env j.uj_val, prterm_env env (incast_type j.uj_type))
+let prjudge = prjudge_env (gLOB nil_sign)
+
 (* Plus de "k"...
 let gentermpr k = gentermpr_core false
 let gentermpr_at_top k = gentermpr_core true
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 67d279867..7d61c7a82 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -24,37 +24,97 @@ open Evarconv
 let mkExistential isevars env =
   new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI
 
-let norec_branch_scheme env isevars typc =
-  let rec crec typc = match whd_betadeltaiota env !isevars typc with 
-    | DOP2(Prod,c,DLAM(name,t)) -> DOP2(Prod,c,DLAM(name,crec t))
-    | _ -> mkExistential isevars env
-  in 
-  crec typc
+let norec_branch_scheme env isevars cstr =
+  prod_it (mkExistential isevars env) cstr.cs_args 
+
+let lift_args l = list_map_i (fun i (name,c) -> (name,liftn 1 i c)) 1 l
 
-let rec_branch_scheme env isevars ((sp,j),_) typc recargs = 
-  let rec crec (typc,recargs) = 
-    match whd_betadeltaiota env !isevars typc, recargs with 
-      | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) -> 
-          DOP2(Prod,c,
+let rec_branch_scheme env isevars ((sp,j),_) recargs cstr = 
+  let rec crec (args,recargs) = 
+    match args, recargs with 
+      | (name,c)::rea,(ra::reca) -> 
+          DOP2(Prod,c,DLAM(name,
 	       match ra with 
-		 | Mrec k -> 
-                     if k=j then 
-		       DLAM(name,mkArrow (mkExistential isevars env)
-                              (crec (lift 1 t,reca)))
-                     else 
-		       DLAM(name,crec (t,reca))
-                 | _ -> DLAM(name,crec (t,reca)))
-      | (_,_) -> mkExistential isevars env
+		 | Mrec k when k=j -> 
+		     mkArrow (mkExistential isevars env)
+		       (crec (lift_args rea,reca))
+                 | _ -> crec (rea,reca)))
+      | [],[] -> mkExistential isevars env
+      | _ -> anomaly "rec_branch_scheme"
   in 
-  crec (typc,recargs) 
+  crec (List.rev cstr.cs_args,recargs) 
     
-let branch_scheme env isevars isrec i (IndFamily (mis,params) as indf) = 
-  let typc = type_inst_construct i indf in 
+let branch_scheme env isevars isrec (IndFamily (mis,params) as indf) =
+  let cstrs = get_constructors indf in 
   if isrec then
-    let recarg = (mis_recarg mis).(i-1) in
-    rec_branch_scheme env isevars (mis_inductive mis) typc recarg
+    array_map2
+      (rec_branch_scheme env isevars (mis_inductive mis))
+      (mis_recarg mis) cstrs
   else 
-    norec_branch_scheme env isevars typc
+    Array.map (norec_branch_scheme env isevars) cstrs
+
+(***************************************************)
+(* Building ML like case expressions without types *)
+
+let concl_n env sigma = 
+  let rec decrec m c = if m = 0 then c else 
+    match whd_betadeltaiota env sigma c with
+      | DOP2(Prod,_,DLAM(n,c_0)) -> decrec (m-1) c_0
+      | _                        -> failwith "Typing.concl_n"
+  in 
+  decrec
+
+let count_rec_arg j = 
+  let rec crec i = function 
+    | [] -> i 
+    | (Mrec k::l) -> crec (if k=j then (i+1) else i) l
+    | (_::l) -> crec i l
+  in 
+  crec 0
+
+(* Used in Program only *)      
+let make_case_ml isrec pred c ci lf = 
+  if isrec then 
+    DOPN(XTRA("REC"),Array.append [|pred;c|] lf)
+  else 
+    mkMutCaseA ci pred c lf
+
+(* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the
+ * K parameters. Then then build_notdep builds the predicate
+ * [a_bar:A'_bar](lift k pred) 
+ * where A'_bar = A_bar[p_bar <- globargs] *)
+
+let build_notdep_pred env sigma indf pred =
+  let arsign,_ = get_arity env sigma indf in
+  let nar = List.length arsign in
+  it_lambda_name env (lift nar pred) arsign
+
+let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
+  let pred =
+    let mispec,_ = dest_ind_family indf in
+    let recargs = mis_recarg mispec in
+    assert (Array.length recargs <> 0);
+    let recargi = recargs.(i) in
+    let j = mis_index mispec in
+    let nbrec = if isrec then count_rec_arg j recargi else 0 in
+    let nb_arg = List.length (recargs.(i)) + nbrec in
+    let pred = concl_n env sigma nb_arg ft in
+    if noccur_between 1 nb_arg pred then 
+      lift (-nb_arg) pred
+    else 
+      failwith "Dependent"
+  in
+  if realargs = [] then 
+    pred
+  else (* we try with [_:T1]..[_:Tn](lift n pred) *)
+    build_notdep_pred env sigma indf pred  
+
+let pred_case_ml env sigma isrec indt lf (i,ft) = 
+    pred_case_ml_fail env sigma isrec indt (i,ft)
+
+(* similar to pred_case_ml but does not expect the list lf of braches *)
+let pred_case_ml_onebranch env sigma isrec indt (i,f,ft) = 
+    pred_case_ml_fail env sigma isrec indt (i,ft)
 
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
@@ -429,7 +489,7 @@ let rec recover_pat_names = function
   | _,[] -> anomaly "Cases.recover_pat_names: Not enough patterns"
 
 let push_rels_eqn sign eqn =
-  let sign' = recover_pat_names (List.rev sign, eqn.patterns) in
+  let sign' = recover_pat_names (sign, eqn.patterns) in
   {eqn with
      rhs = {eqn.rhs with
 	      rhs_env = push_rels sign' eqn.rhs.rhs_env} }
@@ -563,8 +623,8 @@ let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) =
       | Some p -> abstract_predicate env !isevars indf p
       | None -> infer_predicate env isevars typs cstrs indf in
   let typ = applist (pred, realargs) in
-  if dep then (pred, applist (typ, [current]), dummy_sort)
-  else (pred, typ, dummy_sort)
+  if dep then (pred, applist (typ, [current]), Type Univ.dummy_univ)
+  else (pred, typ, Type Univ.dummy_univ)
 
 (************************************************************************)
 (* Sorting equation by constructor *)
@@ -617,8 +677,7 @@ let build_leaf pb =
   let j = pb.typing_function tycon rhs.rhs_env rhs.it in
   let subst = (*List.map (fun id -> (id,make_substituend (List.assoc id rhs.subst))) rhs.user_ids *)[] in
   {uj_val = replace_vars subst j.uj_val;
-   uj_type = replace_vars subst j.uj_type;
-   uj_kind = j.uj_kind}
+   uj_type = typed_app (replace_vars subst) j.uj_type }
 
 (* Building the sub-problem when all patterns are variables *)
 let shift_problem pb =
@@ -703,14 +762,13 @@ and match_current pb (n,tm) =
 	  let tags = Array.map (pattern_status defaults) eqns in
 	  let brs = Array.map compile pbs in
 	  let brvals = Array.map (fun j -> j.uj_val) brs in
-	  let brtyps = Array.map (fun j -> j.uj_type) brs in
+	  let brtyps = Array.map (fun j -> body_of_type j.uj_type) brs in
 	  let (pred,typ,s) =
 	    find_predicate pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt in
 	  let ci = make_case_info mis None tags in
 	  { uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals;
-	    uj_type = typ;
-	    uj_kind = s }
+	    uj_type = make_typed typ s }
 
 and compile_further pb firstnext rest =
   (* We pop as much as possible tomatch not dependent one of the other *)
@@ -718,20 +776,21 @@ and compile_further pb firstnext rest =
   (* the next pattern to match is at the end of [nexts], it has ref (Rel n)
      where n is the length of nexts *)
   let sign = List.map (fun ((na,t),_) -> (na,type_of_tomatch_type t)) nexts in
+  let revsign = List.rev sign in
   let currents =
     list_map_i
       (fun i ((na,t),(_,rhsdep)) ->
 	 Pushed (insert_lifted ((Rel i, lift_tomatch_type i t), rhsdep)))
       1 nexts in
   let pb' = { pb with
-		env = push_rels sign pb.env;
+		env = push_rels revsign pb.env;
 		tomatch = List.rev_append currents future;
                 pred= option_app (weaken_predicate (List.length sign)) pb.pred;
-		mat = List.map (push_rels_eqn sign) pb.mat } in
+		mat = List.map (push_rels_eqn revsign) pb.mat } in
   let j = compile pb' in
   { uj_val = lam_it j.uj_val sign;
-    uj_type = prod_it j.uj_type sign;
-    uj_kind = j.uj_kind }
+    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 }
 
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -799,25 +858,26 @@ let inh_coerce_to_ind isevars env ty tyi =
 
 let coerce_row typing_fun isevars env row tomatch =
   let j = typing_fun empty_tycon env tomatch in
+  let typ = body_of_type j.uj_type in
   let t =
     match find_row_ind row with
 	Some (cloc,(cstr,_ as c)) ->
 	  (let tyi = inductive_of_rawconstructor c in
 	   try 
-	     let indtyp = inh_coerce_to_ind isevars env j.uj_type tyi in
-	     IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
-	 with NotCoercible ->
-	   (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
-	   try
-	     let mind,_ = find_minductype env !isevars j.uj_type in
-	     error_bad_constructor_loc cloc CCI
-	       (constructor_of_rawconstructor c) mind
-	   with Induc ->
-	     error_case_not_inductive_loc
-	       (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type)
+	     let indtyp = inh_coerce_to_ind isevars env typ tyi in
+	     IsInd (typ,find_inductive env !isevars typ)
+	   with NotCoercible ->
+	     (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
+	     try
+	       let mind,_ = find_minductype env !isevars typ in
+	       error_bad_constructor_loc cloc CCI
+		 (constructor_of_rawconstructor c) mind
+	     with Induc ->
+	       error_case_not_inductive_loc
+		 (loc_of_rawconstr tomatch) CCI env j.uj_val typ)
       | None -> 
-	  try IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
-	  with Induc -> NotInd (j.uj_type)
+	  try IsInd (typ,find_inductive env !isevars typ)
+	  with Induc -> NotInd typ
   in (j.uj_val,t)
 
 let coerce_to_indtype typing_fun isevars env matx tomatchl =
@@ -895,9 +955,9 @@ let case_dependent env sigma loc predj tomatchs =
     | (c,NotInd t) ->
 	errorlabstrm "case_dependent" (error_case_not_inductive CCI env c t)
   in
-  let etapred = eta_expand env sigma predj.uj_val predj.uj_type in
+  let etapred = eta_expand env sigma predj.uj_val (body_of_type predj.uj_type) in
   let n = nb_lam etapred in
-  let _,sort = decomp_prod env sigma predj.uj_type in
+  let _,sort = decomp_prod env sigma (body_of_type predj.uj_type) in
   let ndepv = List.map nb_dep_ity tomatchs in
   let sum = List.fold_right (fun i j -> i+j)  ndepv 0 in
   let depsum = sum + List.length tomatchs in
@@ -915,7 +975,7 @@ let prepare_predicate typing_fun isevars env tomatchs = function
       let cdep,arity = case_dependent env !isevars loc predj1 tomatchs in
       (* We got the expected arity of pred and relaunch pretype with it *)
       let predj = typing_fun (mk_tycon arity) env pred in
-      let etapred = eta_expand env !isevars predj.uj_val predj.uj_type in
+      let etapred = eta_expand env !isevars predj.uj_val (body_of_type predj.uj_type) in
       Some (build_initial_predicate cdep etapred tomatchs)
 
 (**************************************************************************)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index fbf77e402..2beb7441c 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -14,7 +14,18 @@ open Evarutil
 (* Used for old cases in pretyping *)
 
 val branch_scheme : 
-  env -> 'a evar_defs -> bool -> int -> inductive_family -> constr
+  env -> 'a evar_defs -> bool -> inductive_family -> constr array
+
+val pred_case_ml_onebranch : env -> 'c evar_map -> bool ->
+  inductive_type -> int * constr * constr -> constr 
+
+(*i Utilisés dans Program
+val pred_case_ml : env -> 'c evar_map -> bool ->
+  constr * (inductive * constr list * constr list)
+  ->  constr array -> int * constr  ->constr
+val make_case_ml :
+  bool -> constr -> constr -> case_info -> constr array -> constr
+i*)
 
 (* Compilation of pattern-matching. *)
 
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 0d011fcce..db67ac2be 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -294,8 +294,8 @@ 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_type_of env Evd.empty t in
-  let vj = {uj_val=v; uj_type=t; uj_kind = k} 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 f_vardep,coef = coe_of_reference v in
   if coercion_exists coef then
     errorlabstrm "try_add_coercion" 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6141d3025..81d8d2cf4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -18,10 +18,9 @@ open Retyping
 
 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_kind=k} =
+let j_nf_ise env sigma {uj_val=v;uj_type=t} =
   { uj_val = nf_ise1 sigma v; 
-    uj_type = nf_ise1 sigma t; 
-    uj_kind = k }
+    uj_type = typed_app (nf_ise1 sigma) t }
 
 let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
 
@@ -29,8 +28,7 @@ let jl_nf_ise env sigma = List.map (j_nf_ise env sigma)
 let apply_coercion_args env argl funj =
   let rec apply_rec acc typ = function
     | [] -> { uj_val=applist(j_val_only funj,argl);
-              uj_type= typ;
-              uj_kind = funj.uj_kind }
+              uj_type= typed_app (fun _ -> typ) funj.uj_type }
     | h::restl ->
       (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
   	match whd_betadeltaiota env Evd.empty typ with
@@ -39,7 +37,7 @@ let apply_coercion_args env argl funj =
 	      apply_rec (h::acc) (subst1 h c2) restl
 	  | _ -> anomaly "apply_coercion_args"
   in 
-  apply_rec [] funj.uj_type argl
+  apply_rec [] (body_of_type funj.uj_type) argl
 
 (* appliquer le chemin de coercions p a` hj *)
 
@@ -55,20 +53,20 @@ let apply_pcoercion env p hj typ_cl =
               let argl = (class_args_of typ_cl)@[ja.uj_val] in
               let jres = apply_coercion_args env argl fv in
               (if b then 
-		 {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val}
+		 { uj_val=ja.uj_val; uj_type=jres.uj_type }
                else 
 		 jres),
-	      jres.uj_type)
+	      (body_of_type jres.uj_type))
            (hj,typ_cl) p)
   with _ -> 
     failwith "apply_pcoercion"
 
 let inh_app_fun env isevars j = 
-  match whd_betadeltaiota env !isevars j.uj_type with
+  match whd_betadeltaiota env !isevars (body_of_type j.uj_type) with
     | DOP2(Prod,_,DLAM(_,_)) -> j
     | _ ->
        	(try
- 	   let t,i1 = class_of1 env !isevars j.uj_type in
+ 	   let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
       	   let p = lookup_path_to_fun_from i1 in
            apply_pcoercion env p j t
 	 with _ -> j)
@@ -76,38 +74,39 @@ let inh_app_fun env isevars j =
 
 let inh_tosort_force env isevars j =
   try
-    let t,i1 = class_of1 env !isevars j.uj_type in
+    let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
     let p = lookup_path_to_sort_from i1 in
     apply_pcoercion env p j t 
   with Not_found -> 
     j
 
 let inh_tosort env isevars j = 
-  let typ = whd_betadeltaiota env !isevars j.uj_type in
+  let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
   match typ with
     | DOP0(Sort _) -> j  (* idem inh_app_fun *)
     | _ -> (try inh_tosort_force env isevars j with _ -> j)
 
 let inh_ass_of_j env isevars j =
-  let typ = whd_betadeltaiota env !isevars j.uj_type in
+  let typ = whd_betadeltaiota env !isevars (body_of_type j.uj_type) in
   match typ with
-    | DOP0(Sort s) -> make_typed j.uj_val s
+    | DOP0(Sort s) -> { utj_val = j.uj_val; utj_type = s }
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
-	assumption_of_judgment env !isevars j1 
+	type_judgment env !isevars j1 
 
 let inh_coerce_to env isevars c1 hj =
   let t1,i1 = class_of1 env !isevars c1 in
-  let t2,i2 = class_of1 env !isevars hj.uj_type in
+  let t2,i2 = class_of1 env !isevars (body_of_type hj.uj_type) in
   let p = lookup_path_between (i2,i1) in
   let hj' = apply_pcoercion env p hj t2 in
-  if the_conv_x_leq env isevars hj'.uj_type c1 then 
+  if the_conv_x_leq env isevars (body_of_type hj'.uj_type) c1 then 
     hj'
   else 
     failwith "inh_coerce_to"
 
 let rec inh_conv_coerce_to env isevars c1 hj =
-  let {uj_val = v; uj_type = t; uj_kind = k} = hj in
+  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 
@@ -130,8 +129,9 @@ let rec inh_conv_coerce_to env isevars c1 hj =
 	       let assv1 = outcast_type v1 in
                let env1 = push_rel (x,assv1) env in
                let h2 = inh_conv_coerce_to env isevars u2
-			  {uj_val = v2; uj_type = t2;
-			   uj_kind = mkSort (get_sort_of env !isevars t2) } in
+			  {uj_val = v2;
+			   uj_type =
+			     make_typed t2 (get_sort_of env !isevars t2) } in
                fst (abs_rel env !isevars x assv1 h2)
              else 
                (* let ju1 = exemeta_rec def_vty_con env isevars u1 in 
@@ -146,36 +146,36 @@ let rec inh_conv_coerce_to env isevars c1 hj =
                let env1 = push_rel (name,assu1) env in
                let h1 = 
 		 inh_conv_coerce_to env isevars t1
-		   {uj_val = Rel 1; uj_type = u1;
-		    uj_kind = mkSort (level_of_type assu1) } in
+		   {uj_val = Rel 1; 
+		    uj_type = typed_app (fun _ -> u1) assu1 } in
                let h2 = inh_conv_coerce_to env isevars u2  
 			 { uj_val = DOPN(AppL,[|(lift 1 v);h1.uj_val|]);
-                           uj_type = subst1 h1.uj_val t2;
-			   uj_kind = mkSort (get_sort_of env !isevars t2) }
+                           uj_type =
+			     make_typed (subst1 h1.uj_val t2)
+			       (get_sort_of env !isevars t2) }
 	       in
 	       fst (abs_rel env !isevars name assu1 h2)
 	 | _ -> failwith "inh_coerce_to")
             
 let inh_cast_rel loc env isevars cj tj =
+  let tj = assumption_of_judgment env !isevars tj in
   let cj' = 
     try 
-      inh_conv_coerce_to env isevars tj.uj_val cj 
+      inh_conv_coerce_to env isevars (body_of_type tj) cj 
     with Not_found | Failure _ -> 
       let rcj = j_nf_ise env !isevars cj in
-      let atj = j_nf_ise env !isevars tj in
-      error_actual_type_loc loc env rcj.uj_val rcj.uj_type atj.uj_type
+      let atj = nf_ise1 !isevars (body_of_type tj) in
+      error_actual_type_loc loc env rcj.uj_val (body_of_type rcj.uj_type) atj
   in
-  { uj_val = mkCast cj'.uj_val tj.uj_val;
-    uj_type = tj.uj_val;
-    uj_kind = whd_betadeltaiota env !isevars tj.uj_type }
+  { uj_val = mkCast cj'.uj_val (body_of_type tj);
+    uj_type = tj }
 
 let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
   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= typ;
-	    uj_kind = funj.uj_kind } 
+	    uj_type= typed_app (fun _ -> typ) funj.uj_type } 
       	in
       	(match vtcon with 
 	   | (_,(_,Some typ')) ->
@@ -193,7 +193,7 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
 		  (try 
 		     inh_conv_coerce_to env isevars c1 hj 
 		   with Failure _ | Not_found ->
-                     error_cant_apply_bad_type_loc apploc env (n,c1,hj.uj_type)
+                     error_cant_apply_bad_type_loc apploc env (n,c1,(body_of_type hj.uj_type))
 		       (j_nf_ise env !isevars funj)
 		       (jl_nf_ise env !isevars argjl)) 
 	      in
@@ -202,5 +202,5 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
               error_cant_apply_not_functional_loc apploc env
 	      	(j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)
   in 
-  apply_rec 1 [] funj.uj_type argjl
+  apply_rec 1 [] (body_of_type funj.uj_type) argjl
 
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index cb892ed7c..ec1ab927b 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -18,7 +18,7 @@ val inh_tosort_force :
 val inh_tosort :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_ass_of_j : 
-  env -> 'a evar_defs -> unsafe_judgment -> typed_type
+  env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
 val inh_coerce_to : 
   env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment
 val inh_conv_coerce_to : 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 863843d4f..1b2d287b1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -81,7 +81,7 @@ let split_evar_to_arrow sigma c =
   let dsp = num_of_evar (body_of_type dom) in
   let rsp = num_of_evar (body_of_type rng) in
   (sigma3,
-   make_typed (mkEvar dsp args) (Type dummy_univ),
+   { utj_val = mkEvar dsp args; utj_type = Type dummy_univ },
    mkCast (mkEvar rsp (array_cons (mkRel 1) args)) dummy_sort)
 
 
@@ -377,7 +377,7 @@ let status_changed lev (pbty,t1,t2) =
 
 (* Operations on value/type constraints used in trad and progmach *)
 
-type trad_constraint = bool * (typed_type option * constr option)
+type trad_constraint = bool * (unsafe_type_judgment option * constr option)
 
 (* Basically, we have the following kind of constraints (in increasing
  * strength order):
@@ -416,8 +416,12 @@ let prod_dom_tycon_unif env isevars = function
          | DOP2(Prod,c1,_) ->
 	     let t =
 	       match c1 with 
-		 | DOP2 (Cast,cc1,DOP0 (Sort s)) -> make_typed cc1 s
-		 | _  -> make_typed c1 (Retyping.get_sort_of env !isevars c1)
+		 | DOP2 (Cast,cc1,DOP0 (Sort s)) ->
+		     { utj_val = cc1;
+		       utj_type = s }
+		 | _  ->
+		     { utj_val = c1;
+		       utj_type = Retyping.get_sort_of env !isevars c1 }
 	     in Some t
 	 | t ->
 	     if (ise_undefined isevars t) then begin
@@ -431,7 +435,11 @@ let prod_dom_tycon_unif env isevars = function
  * first argument. *) 
 
 let app_dom_tycon env isevars (_,(_,tyc)) =
-  (false,(None, option_app incast_type (prod_dom_tycon_unif env isevars tyc)))
+  (false,
+   (None, 
+    option_app
+      (fun x -> incast_type (Typeops.assumption_of_type_judgment x))
+	   (prod_dom_tycon_unif env isevars tyc)))
 
 
 (* Given a constraint on a term, returns the constraint corresponding to this
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 0758210b1..d9d3dc41b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -50,7 +50,7 @@ val status_changed : int list -> conv_pb * constr * constr -> bool
 
 (* Value/Type constraints *)
 
-type trad_constraint = bool * (typed_type option * constr option)
+type trad_constraint = bool * (unsafe_type_judgment option * constr option)
 
 val empty_tycon : trad_constraint
 val def_vty_con : trad_constraint
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 72eed91c5..23e7b5682 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -136,8 +136,8 @@ let mt_evd = Evd.empty
 
 let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
 
-let j_nf_ise sigma {uj_val=v;uj_type=t;uj_kind=k} =
-  {uj_val=nf_ise1 sigma v;uj_type=nf_ise1 sigma t;uj_kind=k}
+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}
 
 let jv_nf_ise sigma = Array.map (j_nf_ise sigma)
 
@@ -151,7 +151,8 @@ 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
-		  (vdefj.(i)).uj_type (lift lt (body_of_type lar.(i)))) then
+		  (body_of_type (vdefj.(i)).uj_type)
+		  (lift lt (body_of_type 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)
@@ -197,12 +198,10 @@ let pretype_var loc env lvar id =
          match lookup_id id (context env) with
            | RELNAME (n,typ) ->
 	     { 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 }
            | GLOBNAME (id,typ) ->
 	     { uj_val  = VAR id;
-	       uj_type = body_of_type typ;
-	       uj_kind = DOP0 (Sort (level_of_type typ)) }
+	       uj_type = typ }
       with Not_found ->
         error_var_not_found_loc loc CCI id);;
 
@@ -251,12 +250,14 @@ let pretype_ref pretype loc isevars env lvar = function
  
 | RConstruct (cstr_sp,ctxt) ->
     let cstr = (cstr_sp,Array.map pretype ctxt) in
-    let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in
-    {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind}
+    let typ = type_of_constructor env !isevars cstr in
+    { uj_val=mkMutConstruct cstr; uj_type=typ }
 
 let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
-  | RType -> { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort}
+  | RType ->
+      { uj_val = dummy_sort;
+	uj_type = make_typed dummy_sort (Type Univ.dummy_univ) }
 
 (* pretype vtcon isevars env constr tries to solve the *)
 (* existential variables in constr in environment env with the *)
@@ -284,26 +285,22 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	  in
             (match kind_of_term metaty with
                 IsCast (typ,kind) ->
-                  {uj_val=DOP0 (Meta n); uj_type=typ; uj_kind=kind}
-               | _ ->
-                 {uj_val=DOP0 (Meta n);
-                  uj_type=metaty;
-                  uj_kind=failwith "should be casted"}))
+                  { uj_val=DOP0 (Meta n); uj_type = outcast_type metaty }
+               | _ -> failwith "should be casted"))
 	          (* hnf_constr !isevars (exemeta_hack metaty).uj_type}) *)
 
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
   (match vtcon with
     (true,(Some v, _)) ->
-      let (valc,typc) = (body_of_type v,mkSort (level_of_type v)) in
-      {uj_val=valc; uj_type=typc; uj_kind=dummy_sort}
+      {uj_val=v.utj_val; uj_type=make_typed (mkSort v.utj_type) (Type Univ.dummy_univ)}
   | (false,(None,Some ty)) ->
       let c = new_isevar isevars env ty CCI in
-      {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
+      {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
   | (true,(None,None)) ->
       let ty = mkCast dummy_sort dummy_sort in
       let c = new_isevar isevars env ty CCI in
-      {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
+      {uj_val=c;uj_type=make_typed ty (Type Univ.dummy_univ)}
   | (false,(None,None)) ->
       (match loc with
 	  None -> anomaly "There is an implicit argument I cannot solve"
@@ -351,13 +348,13 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       let rtc = app_rng_tycon env isevars cj.uj_val tycon in
       (rtc,cj::jl)  in
     let jl = List.rev (snd (List.fold_left apply_one_arg
-			      (mk_tycon j.uj_type,[]) args)) in
+			      (mk_tycon (incast_type j.uj_type),[]) args)) in
     inh_apply_rel_list !trad_nocheck loc env isevars jl j vtcon
 
 | RBinder(loc,BLambda,name,c1,c2)      ->
     let j =
       pretype (abs_dom_valcon env isevars vtcon) env isevars lvar lmeta c1 in
-    let assum = inh_ass_of_j env isevars j in
+    let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
     let var = (name,assum) in
     let j' =
       pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars lvar
@@ -368,7 +365,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | RBinder(loc,BProd,name,c1,c2)        ->
     let j = pretype def_vty_con env isevars lvar lmeta c1 in
     let assum = inh_ass_of_j env isevars j in
-    let var = (name,assum) in
+    let var = (name,assumption_of_type_judgment assum) in
     let j' = pretype def_vty_con (push_rel var env) isevars lvar lmeta c2 in
     let j'' = inh_tosort env isevars j' in
     fst (gen_rel env !isevars name assum j'')
@@ -376,47 +373,50 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | 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_inductive env !isevars cj.uj_type
+    try find_inductive env !isevars (body_of_type cj.uj_type)
     with Induc -> error_case_not_inductive CCI env
-	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
+	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars (body_of_type cj.uj_type)) in
   let pj = match po with
     | Some p -> pretype empty_tycon env isevars lvar lmeta p
     | None -> 
 	try match vtcon with
 	    (_,(_,Some pred)) -> 
 	      let (predc,predt) = destCast pred in
-	      let predj = {uj_val=predc;uj_type=predt;uj_kind=dummy_sort} in
+	      let predj =
+		{ uj_val=predc;
+		  uj_type=make_typed predt (Type Univ.dummy_univ) } in
 	      inh_tosort env isevars predj
 	  | _ -> error "notype"
 	with UserError _ -> (* get type information from type of branches *)
+	  let expbr = Cases.branch_scheme env isevars isrec indf in
 	  let rec findtype i =
-	    if i > Array.length lf
+	    if i >= Array.length lf
 	    then error_cant_find_case_type_loc loc env cj.uj_val
 	    else
 	      try
-		let expti = Cases.branch_scheme env isevars isrec i indf in
+		let expti = expbr.(i) in
 		let fj =
-                  pretype (mk_tycon expti) env isevars lvar lmeta lf.(i-1) in
-		let efjt = nf_ise1 !isevars fj.uj_type in 
+                  pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in
+		let efjt = nf_ise1 !isevars (body_of_type fj.uj_type) in 
 		let pred = 
-		  Indrec.pred_case_ml_onebranch env !isevars isrec indt
+		  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
-		  let k = Retyping.get_type_of env !isevars pty in
-		    {uj_val=pred;uj_type=pty;uj_kind=k}
+		  let k = Retyping.get_sort_of env !isevars pty in
+		    { uj_val=pred; uj_type=make_typed pty k }
 	      with UserError _ -> findtype (i+1) in
-	    findtype 1 in
+	    findtype 0 in
 
-  let evalct = find_inductive env !isevars cj.uj_type (*Pour normaliser evars*)
-  and evalPt = nf_ise1 !isevars pj.uj_type in
+  let evalct = find_inductive env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
+  and evalPt = nf_ise1 !isevars (body_of_type 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 cj.uj_type)
+      (cj.uj_val,nf_ise1 !isevars (body_of_type cj.uj_type))
       (Array.length bty)
   else
     let lfj =
@@ -424,7 +424,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
         (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 -> j.uj_type) lfj) in
+    let lft = (Array.map (fun j -> body_of_type j.uj_type) lfj) in
     check_branches_message loc env isevars cj.uj_val (bty,lft);
     let v =
       if isrec
@@ -435,9 +435,9 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	let ci = make_default_case_info mis in
 	mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj)
     in
+    let s = destSort (snd (splay_prod env !isevars evalPt)) in
     {uj_val = v;
-     uj_type = rsty;
-     uj_kind = snd (splay_prod env !isevars evalPt)}
+     uj_type = make_typed rsty s }
 
 | RCases (loc,prinfo,po,tml,eqns) ->
     Cases.compile_cases
@@ -482,8 +482,7 @@ let j_apply f env sigma j =
     | DOP2 (Cast,b,t) -> DOP2 (Cast,f env sigma b,f env sigma t)
     | c -> f env sigma c in
   { uj_val=strong (under_outer_cast f) env sigma j.uj_val;
-    uj_type=strong f env sigma j.uj_type;
-    uj_kind=strong f env sigma j.uj_kind}
+    uj_type= typed_app (strong f env sigma) j.uj_type }
 
 (* TODO: comment faire remonter l'information si le typage a resolu des
        variables du sigma original. il faudrait que la fonction de typage
@@ -509,7 +508,7 @@ let ise_resolve fail_evar sigma metamap env lvar lmeta c =
 let ise_resolve_type fail_evar sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine def_vty_con false isevars metamap env [] [] c in
-  let tj = inh_ass_of_j env isevars j in
+  let tj = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
   typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj
 
 let ise_resolve_nocheck sigma metamap env c =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index e4554527d..b90dc602b 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -46,11 +46,10 @@ let rec type_of env cstr=
     | IsRel n -> lift n (body_of_type (snd (lookup_rel n env)))
     | IsVar id -> body_of_type (snd (lookup_var id env))
     | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*)
-    | IsConst c -> (body_of_type (type_of_constant env sigma c))
+    | IsConst c -> body_of_type (type_of_constant env sigma c)
     | IsEvar _ -> type_of_existential env sigma cstr
-    | IsMutInd ind -> (body_of_type (type_of_inductive env sigma ind))
-    | IsMutConstruct cstr -> 
-        let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
+    | IsMutInd ind -> body_of_type (type_of_inductive env sigma ind)
+    | IsMutConstruct cstr -> body_of_type (type_of_constructor env sigma cstr)
     | IsMutCase (_,p,c,lf) ->
         let IndType (indf,realargs) =
           try find_inductive env sigma (type_of env c)
@@ -97,4 +96,4 @@ let get_type_of_with_meta env sigma metamap = fst (typeur sigma metamap) env
 let mk_unsafe_judgment env evc c=
   let typ=get_type_of env evc c
   in
-    {uj_val=c;uj_type=typ;uj_kind=(mkSort (get_sort_of env evc typ))};;
+    {uj_val=c;uj_type=make_typed typ (get_sort_of env evc typ)};;
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 92ad4cf5c..873939c91 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -28,7 +28,8 @@ let rec execute mf env sigma cstr =
     | IsEvar _ ->
 	let ty = type_of_existential env sigma cstr in
 	let jty = execute mf env sigma ty in
-	{ uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type }
+	let jty = assumption_of_judgment env sigma jty in
+	{ uj_val = cstr; uj_type = jty }
 	
     | IsRel n -> 
 	relative env n
@@ -49,8 +50,7 @@ let rec execute mf env sigma cstr =
 	make_judge cstr (type_of_inductive env sigma ind)
 	  
     | IsMutConstruct cstruct -> 
-	let (typ,kind) = destCast (type_of_constructor env sigma cstruct) in
-        { uj_val = cstr; uj_type = typ; uj_kind = kind }
+	make_judge cstr (type_of_constructor env sigma cstruct)
 	  
     | IsMutCase (ci,p,c,lf) ->
         let cj = execute mf env sigma c in
@@ -88,7 +88,7 @@ let rec execute mf env sigma cstr =
 	    
     | IsLambda (name,c1,c2) -> 
         let j = execute mf env sigma c1 in
-        let var = assumption_of_judgment env sigma j in
+	let var = assumption_of_judgment env sigma j in
 	let env1 = push_rel (name,var) env in
         let j' = execute mf env1 sigma c2 in 
         let (j,_) = abs_rel env1 sigma name var j' in
@@ -96,10 +96,11 @@ let rec execute mf env sigma cstr =
 	  
     | IsProd (name,c1,c2) ->
         let j = execute mf env sigma c1 in
-        let var = assumption_of_judgment env sigma j in
+        let varj = type_judgment env sigma j in
+	let var = assumption_of_type_judgment varj in
 	let env1 = push_rel (name,var) env in
         let j' = execute mf env1 sigma c2 in
-	let (j,_) = gen_rel env1 sigma name var j' in
+	let (j,_) = gen_rel env1 sigma name varj j' in
 	j
 	  
     | IsCast (c,t) ->
@@ -146,7 +147,7 @@ let unsafe_machine env sigma constr =
 
 let type_of env sigma c = 
   let j = safe_machine env sigma c in 
-  nf_betaiota env sigma j.uj_type
+  nf_betaiota env sigma (body_of_type j.uj_type)
 
 (* The typed type of a judgment. *)