Abstraction du type typed_type (un pas vers les jugements 2 niveaux)

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

13 files changed, 308 insertions, 265 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ab7263503..e48e9dc97 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -16,6 +16,94 @@ open Typeops
    is given, since inductive types are typed in an environment without 
    existentials. *)
 
+(* [check_constructors_names id s cl] checks that all the constructors names
+   appearing in [l] are not present in the set [s], and returns the new set
+   of names. The name [id] is the name of the current inductive type, used
+   when reporting the error. *)
+
+(***********************************************************************)
+(* Various well-formedness check for inductive declarations            *)
+
+type inductive_error =
+  | NonPos of name list * constr * constr
+  | NotEnoughArgs of name list * constr * constr
+  | NotConstructor of name list * constr * constr
+  | NonPar of name list * constr * int * constr * constr
+  | SameNamesTypes of identifier
+  | SameNamesConstructors of identifier * identifier
+  | NotAnArity of identifier
+  | BadEntry
+
+exception InductiveError of inductive_error
+
+let check_constructors_names id =
+  let rec check idset = function
+    | [] -> idset
+    | c::cl -> 
+	if Idset.mem c idset then 
+	  raise (InductiveError (SameNamesConstructors (id,c)))
+	else
+	  check (Idset.add c idset) cl
+  in
+  check
+
+(* [mind_check_names mie] checks the names of an inductive types declaration,
+   and raises the corresponding exceptions when two types or two constructors
+   have the same name. *)
+
+let mind_check_names mie =
+  let rec check indset cstset = function
+    | [] -> ()
+    | (id,_,cl,_)::inds -> 
+	if Idset.mem id indset then
+	  raise (InductiveError (SameNamesTypes id))
+	else
+	  let cstset' = check_constructors_names id cstset cl in
+	  check (Idset.add id indset) cstset' inds
+  in
+  check Idset.empty Idset.empty mie.mind_entry_inds
+
+(* [mind_extract_params mie] extracts the params from an inductive types
+   declaration, and checks that they are all present (and all the same)
+   for all the given types. *)
+
+let mind_extract_params n c =
+  let (l,c') = decompose_prod_n n c in (List.rev l,c')
+  
+let extract nparams c =
+  try mind_extract_params nparams c 
+  with UserError _ -> raise (InductiveError BadEntry)
+
+let check_params nparams params c = 
+  let eparams = fst (extract nparams c) in
+  try
+    List.iter2 
+      (fun (n1,t1) (n2,t2) ->
+	 if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
+	   raise (InductiveError BadEntry))
+      eparams params
+  with Invalid_argument _ ->
+    raise (InductiveError BadEntry)
+
+let mind_extract_and_check_params mie =
+  let nparams = mie.mind_entry_nparams in
+  match mie.mind_entry_inds with
+    | [] -> anomaly "empty inductive types declaration"
+    | (_,ar,_,_)::l -> 
+	let (params,_) = extract nparams ar in
+	List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
+	params
+
+let mind_check_lc params mie =
+  let ntypes = List.length mie.mind_entry_inds in
+  let nparams = List.length params in
+  let check_lc (_,_,_,lc) =
+    let (lna,c) = decomp_all_DLAMV_name lc in
+    Array.iter (check_params nparams params) c;
+    if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
+  in
+  List.iter check_lc mie.mind_entry_inds
+
 let mind_check_arities env mie =
   let check_arity id c =
     if not (is_arity env Evd.empty c) then 
@@ -23,6 +111,8 @@ let mind_check_arities env mie =
   in
   List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
 
+(***********************************************************************)
+
 let allowed_sorts issmall isunit = function
   | Type _ -> 
       [prop;spec;types]
@@ -34,10 +124,10 @@ let allowed_sorts issmall isunit = function
 let is_small_type t = is_small t.typ
 
 type ill_formed_ind =
-  | NonPos of int
-  | NotEnoughArgs of int
-  | NotConstructor
-  | NonPar of int * int
+  | LocalNonPos of int
+  | LocalNotEnoughArgs of int
+  | LocalNotConstructor
+  | LocalNonPar of int * int
 
 exception IllFormedInd of ill_formed_ind
 
@@ -45,33 +135,33 @@ let explain_ind_err ntyp lna nbpar c err =
   let (lpar,c') = mind_extract_params nbpar c in
   let env = (List.map fst lpar)@lna in
   match err with
-    | NonPos kt -> 
-	raise (InductiveError (Inductive.NonPos (env,c',Rel (kt+nbpar))))
-    | NotEnoughArgs kt -> 
+    | LocalNonPos kt -> 
+	raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
+    | LocalNotEnoughArgs kt -> 
 	raise (InductiveError 
-		 (Inductive.NotEnoughArgs (env,c',Rel (kt+nbpar))))
-    | NotConstructor ->
+		 (NotEnoughArgs (env,c',Rel (kt+nbpar))))
+    | LocalNotConstructor ->
 	raise (InductiveError 
-		 (Inductive.NotConstructor (env,c',Rel (ntyp+nbpar))))
-    | NonPar (n,l) ->
+		 (NotConstructor (env,c',Rel (ntyp+nbpar))))
+    | LocalNonPar (n,l) ->
 	raise (InductiveError 
-		 (Inductive.NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
+		 (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
 
 let failwith_non_pos_vect n ntypes v =
   for i = 0 to Array.length v - 1 do
     for k = n to n + ntypes - 1 do
-      if not (noccurn k v.(i)) then raise (IllFormedInd (NonPos (k-n+1)))
+      if not (noccurn k v.(i)) then raise (IllFormedInd (LocalNonPos (k-n+1)))
     done
   done;
   anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v"
 
 let check_correct_par env nparams ntypes n l largs =
   if Array.length largs < nparams then 
-    raise (IllFormedInd (NotEnoughArgs l));
+    raise (IllFormedInd (LocalNotEnoughArgs l));
   let (lpar,largs') = array_chop nparams largs in
   for k = 0 to nparams - 1 do
     if not ((Rel (n-k-1))= whd_betadeltaiotaeta env Evd.empty lpar.(k)) then
-      raise (IllFormedInd (NonPar (k+1,l)))
+      raise (IllFormedInd (LocalNonPar (k+1,l)))
   done;
   if not (array_for_all (noccur_bet n ntypes) largs') then 
     failwith_non_pos_vect n ntypes largs'
@@ -95,7 +185,7 @@ let listrec_mconstr env ntypes nparams i indlc =
   let rec check_pos n c = 
     match whd_betadeltaiota env Evd.empty c with 
       | DOP2(Prod,b,DLAM(na,d)) -> 
-          if not (noccur_bet n ntypes b) then raise (IllFormedInd (NonPos n));
+          if not (noccur_bet n ntypes b) then raise (IllFormedInd (LocalNonPos n));
 	  check_pos (n+1) d
       | x -> 
 	  let hd,largs = destApplication (ensure_appl x) in
@@ -109,23 +199,23 @@ let listrec_mconstr env ntypes nparams i indlc =
 		  then Param(n-1-k)
                   else Norec
 		else
-		  raise (IllFormedInd (NonPos n))
+		  raise (IllFormedInd (LocalNonPos n))
             | DOPN(MutInd ind_sp,a) -> 
                 if (noccur_bet n ntypes x) then Norec
                 else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
             | err -> 
 		if noccur_bet n ntypes x then Norec
-		else raise (IllFormedInd (NonPos n))
+		else raise (IllFormedInd (LocalNonPos n))
 
   and imbr_positive n mi largs =
     let mispeci = lookup_mind_specif mi env in
     let auxnpar = mis_nparams mispeci in
     let (lpar,auxlargs) = array_chop auxnpar largs in 
     if not (array_for_all (noccur_bet n ntypes) auxlargs) then
-      raise (IllFormedInd (NonPos n));
+      raise (IllFormedInd (LocalNonPos n));
     let auxlc = mis_lc mispeci 
     and auxntyp = mis_ntypes mispeci in 
-    if auxntyp <> 1 then raise (IllFormedInd (NonPos n));
+    if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
     let lrecargs = array_map_to_list (check_weak_pos n) lpar in
     (* The abstract imbricated inductive type with parameters substituted *)
     let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
@@ -165,7 +255,7 @@ let listrec_mconstr env ntypes nparams i indlc =
       | DOP2(Lambda,b,DLAM(na,d)) -> 
           if noccur_bet n ntypes b
           then check_weak_pos (n+1) d
-          else raise (IllFormedInd (NonPos n))
+          else raise (IllFormedInd (LocalNonPos n))
       (******************)
       | x -> check_pos n x
   
@@ -185,10 +275,10 @@ let listrec_mconstr env ntypes nparams i indlc =
               match hd with
 		| Rel k when k = n+ntypes-i ->
 		    check_correct_par env nparams ntypes n (k-n+1) largs
-                | _ -> raise (IllFormedInd NotConstructor)
+                | _ -> raise (IllFormedInd LocalNotConstructor)
 	    else
 	      if not (array_for_all (noccur_bet n ntypes) largs)
-              then raise (IllFormedInd (NonPos n));
+              then raise (IllFormedInd (LocalNonPos n));
 	    List.rev lrec
     in check_constr_rec []
   in
@@ -215,7 +305,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
   let one_packet i (id,ar,cnames,issmall,isunit,lc) =
     let recargs = listrec_mconstr env_ar ntypes nparams i lc in
     let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
-    let (ar_sign,ar_sort) = splay_arity env Evd.empty ar.body in
+    let (ar_sign,ar_sort) = splay_arity env Evd.empty (body_of_type ar) in
     let kelim = allowed_sorts issmall isunit ar_sort in
     { mind_consnames = Array.of_list cnames;
       mind_typename = id;
@@ -229,7 +319,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
   let ids = 
     List.fold_left 
       (fun acc (_,ar,_,_,_,lc) -> 
-	 Idset.union (global_vars_set ar.body) 
+	 Idset.union (global_vars_set (body_of_type ar)) 
 	   (Idset.union (global_vars_set lc) acc))
       Idset.empty inds
   in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 1e675b2c0..e955f6009 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,11 +9,50 @@ open Inductive
 open Environ
 (*i*)
 
+
+(*s The different kinds of errors that may result of a malformed inductive
+  definition. *)
+
+type inductive_error =
+  | NonPos of name list * constr * constr
+  | NotEnoughArgs of name list * constr * constr
+  | NotConstructor of name list * constr * constr
+  | NonPar of name list * constr * int * constr * constr
+  | SameNamesTypes of identifier
+  | SameNamesConstructors of identifier * identifier
+  | NotAnArity of identifier
+  | BadEntry
+
+exception InductiveError of inductive_error
+
+(*s The following functions are utility functions to check and to
+  decompose a declaration. *)
+
+(* [mind_check_names] checks the names of an inductive types declaration
+   i.e. that all the types and constructors names are distinct. 
+   It raises an exception [InductiveError _] if it is not the case. *)
+
+val mind_check_names : mutual_inductive_entry -> unit
+
+(* [mind_extract_and_check_params] extracts the parameters of an inductive
+   types declaration. It raises an exception [InductiveError _] if there is
+   not enough abstractions in any of the terms of the field 
+   [mind_entry_inds]. *)
+
+val mind_extract_and_check_params : 
+  mutual_inductive_entry -> (name * constr) list
+
+val mind_extract_params : int -> constr -> (name * constr) list * constr
+
+val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+
 (* [mind_check_arities] checks that the types declared for all the
    inductive types are some arities. *)
 
 val mind_check_arities : env -> mutual_inductive_entry -> unit
 
+(* [cci_inductive] checks positivity and builds an inductive body *)
+
 val cci_inductive : 
   env -> env -> path_kind -> int -> bool -> 
     (identifier * typed_type * identifier list * bool * bool * constr) list ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fda1190d1..9a59a889b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -106,91 +106,6 @@ type mutual_inductive_entry = {
   mind_entry_finite : bool;
   mind_entry_inds : (identifier * constr * identifier list * constr) list }
 
-type inductive_error =
-  | NonPos of name list * constr * constr
-  | NotEnoughArgs of name list * constr * constr
-  | NotConstructor of name list * constr * constr
-  | NonPar of name list * constr * int * constr * constr
-  | SameNamesTypes of identifier
-  | SameNamesConstructors of identifier * identifier
-  | NotAnArity of identifier
-  | BadEntry
-
-exception InductiveError of inductive_error
-
-(* [check_constructors_names id s cl] checks that all the constructors names
-   appearing in [l] are not present in the set [s], and returns the new set
-   of names. The name [id] is the name of the current inductive type, used
-   when reporting the error. *)
-
-let check_constructors_names id =
-  let rec check idset = function
-    | [] -> idset
-    | c::cl -> 
-	if Idset.mem c idset then 
-	  raise (InductiveError (SameNamesConstructors (id,c)))
-	else
-	  check (Idset.add c idset) cl
-  in
-  check
-
-(* [mind_check_names mie] checks the names of an inductive types declaration,
-   and raises the corresponding exceptions when two types or two constructors
-   have the same name. *)
-
-let mind_check_names mie =
-  let rec check indset cstset = function
-    | [] -> ()
-    | (id,_,cl,_)::inds -> 
-	if Idset.mem id indset then
-	  raise (InductiveError (SameNamesTypes id))
-	else
-	  let cstset' = check_constructors_names id cstset cl in
-	  check (Idset.add id indset) cstset' inds
-  in
-  check Idset.empty Idset.empty mie.mind_entry_inds
-
-(* [mind_extract_params mie] extracts the params from an inductive types
-   declaration, and checks that they are all present (and all the same)
-   for all the given types. *)
-
-let mind_extract_params n c = 
-  let (l,c') = decompose_prod_n n c in (List.rev l,c')
-  
-let extract nparams c =
-  try mind_extract_params nparams c 
-  with UserError _ -> raise (InductiveError BadEntry)
-
-let check_params nparams params c = 
-  let eparams = fst (extract nparams c) in
-  try
-    List.iter2 
-      (fun (n1,t1) (n2,t2) ->
-	 if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
-	   raise (InductiveError BadEntry))
-      eparams params
-  with Invalid_argument _ ->
-    raise (InductiveError BadEntry)
-
-let mind_extract_and_check_params mie =
-  let nparams = mie.mind_entry_nparams in
-  match mie.mind_entry_inds with
-    | [] -> anomaly "empty inductive types declaration"
-    | (_,ar,_,_)::l -> 
-	let (params,_) = extract nparams ar in
-	List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
-	params
-
-let mind_check_lc params mie =
-  let ntypes = List.length mie.mind_entry_inds in
-  let nparams = List.length params in
-  let check_lc (_,_,_,lc) =
-    let (lna,c) = decomp_all_DLAMV_name lc in
-    Array.iter (check_params nparams params) c;
-    if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
-  in
-  List.iter check_lc mie.mind_entry_inds
-
 let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
 let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c9857daaf..c5520cf49 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -112,42 +112,6 @@ type mutual_inductive_entry = {
   mind_entry_finite : bool;
   mind_entry_inds : (identifier * constr * identifier list * constr) list }
 
-(*s The different kinds of errors that may result of a malformed inductive
-  definition. *)
-
-type inductive_error =
-  | NonPos of name list * constr * constr
-  | NotEnoughArgs of name list * constr * constr
-  | NotConstructor of name list * constr * constr
-  | NonPar of name list * constr * int * constr * constr
-  | SameNamesTypes of identifier
-  | SameNamesConstructors of identifier * identifier
-  | NotAnArity of identifier
-  | BadEntry
-
-exception InductiveError of inductive_error
-
-(*s The following functions are utility functions to check and to
-  decompose a declaration. *)
-
-(* [mind_check_names] checks the names of an inductive types declaration
-   i.e. that all the types and constructors names are distinct. 
-   It raises an exception [InductiveError _] if it is not the case. *)
-
-val mind_check_names : mutual_inductive_entry -> unit
-
-(* [mind_extract_and_check_params] extracts the parameters of an inductive
-   types declaration. It raises an exception [InductiveError _] if there is
-   not enough abstractions in any of the terms of the field 
-   [mind_entry_inds]. *)
-
-val mind_extract_and_check_params : 
-  mutual_inductive_entry -> (name * constr) list
-
-val mind_extract_params : int -> constr -> (name * constr) list * constr
-
-val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
-
 val inductive_of_constructor : constructor -> inductive
 
 val ith_constructor_of_inductive : inductive -> int -> constructor
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index bf3135790..5e48b8e0c 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -26,33 +26,34 @@ let instantiate_constr ids c args =
     replace_vars (List.combine ids (List.map make_substituend args)) c
 
 let instantiate_type ids tty args =
-  { body = instantiate_constr ids tty.body args;
-    typ = tty.typ }
+  typed_app (fun c -> instantiate_constr ids c args) tty
 
 (* Constants. *)
 
 (* constant_type gives the type of a constant *)
-let constant_type env k =
-  let (sp,args) = destConst k in
+let constant_type env sigma (sp,args) =
   let cb = lookup_constant sp env in
+  (* TODO: check args *)
   instantiate_type 
     (ids_of_sign cb.const_hyps) cb.const_type (Array.to_list args)
 
-let constant_value env k =
-  let (sp,args) = destConst k in
-  let cb = lookup_constant sp env in
-  if not cb.const_opaque & defined_constant env k then
-    match cb.const_body with
-      | Some v -> 
-	  let body = cook_constant v in
-          instantiate_constr 
-	    (ids_of_sign cb.const_hyps) body (Array.to_list args)
-      | None -> 
-	  anomalylabstrm "termenv__constant_value"
-	    [< 'sTR "a defined constant with no body." >]
-  else 
-    failwith "opaque"
+type const_evaluation_error = NotDefinedConst | OpaqueConst
+
+exception NotEvaluableConst of const_evaluation_error
 
+let constant_value env cst =
+  let (sp,args) = destConst cst in
+  let cb = lookup_constant sp env in
+  if cb.const_opaque then raise (NotEvaluableConst OpaqueConst) else
+  if not (is_defined cb) then raise (NotEvaluableConst NotDefinedConst) else
+  match cb.const_body with
+    | Some v -> 
+	let body = cook_constant v in
+        instantiate_constr 
+	  (ids_of_sign cb.const_hyps) body (Array.to_list args)
+    | None ->
+	anomalylabstrm "termenv__constant_value"
+	  [< 'sTR "a defined constant with no body." >]
 
 let mis_lc mis =
   instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
@@ -115,7 +116,6 @@ let mis_typed_arity mis =
   and largs = Array.to_list mis.mis_args in
   instantiate_type idhyps mis.mis_mip.mind_arity largs
 
-let mis_arity mispec =
-  let { body = b; typ = t } = mis_typed_arity mispec in
-  DOP2 (Cast, b, DOP0 (Sort t))
+let mis_arity mispec = incast_type (mis_typed_arity mispec)
+
 
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 9f5b02e92..8d267021f 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -16,8 +16,13 @@ val instantiate_constr :
 val instantiate_type : 
   identifier list -> typed_type -> constr list -> typed_type
 
+type const_evaluation_error = NotDefinedConst | OpaqueConst
+exception NotEvaluableConst of const_evaluation_error
+
+(* [constant_value env c] raises [NotEvaluableConst OpaqueConst] if
+   [c] is opaque and [NotEvaluableConst NotDefinedConst] if undefined *)
 val constant_value : env -> constr -> constr
-val constant_type : env -> constr -> typed_type
+val constant_type : env -> 'a evar_map -> constant -> typed_type
 
 val existential_value : 'a evar_map -> constr -> constr
 val existential_type : 'a evar_map -> constr -> constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6f41a3c64..caf667dae 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1227,10 +1227,10 @@ let is_type_arity env sigma =
   srec 
 
 let is_info_type env sigma t =
-  let s = t.typ in
+  let s = level_of_type t in
   (s = Prop Pos) ||
   (s <> Prop Null && 
-   try info_arity env sigma t.body with IsType -> true)
+   try info_arity env sigma (body_of_type t) with IsType -> true)
 
 let is_info_cast_type env sigma c = 
   match c with  
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e855e443..0f0907786 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -110,7 +110,7 @@ let rec execute mf env cstr =
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
 	(j, cst)
 	  
-    | IsProd (name,c1,c2) ->
+     | IsProd (name,c1,c2) ->
         let (j,cst1) = execute mf env c1 in
         let var = assumption_of_judgment env Evd.empty j in
 	let env1 = push_rel (name,var) env in
@@ -156,8 +156,8 @@ and execute_list mf env = function
 (* The typed type of a judgment. *)
 
 let execute_type mf env constr = 
-  let (j,_) = execute mf env constr in
-  assumption_of_judgment env Evd.empty j
+  let (j,cst) = execute mf env constr in
+  (assumption_of_judgment env Evd.empty j, cst)
 
 
 (* Exported machines.  First safe machines, with no general fixpoint
@@ -198,15 +198,16 @@ let unsafe_machine_type env constr =
 let type_of env c = 
   let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type
 
+(* obsolètes
 let type_of_type env c = 
-  let tt = safe_machine_type env c in DOP0 (Sort tt.typ)
+  let tt = safe_machine_type env c in DOP0 (Sort (level_of_type tt.typ)
 
 let unsafe_type_of env c = 
   let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type
 
 let unsafe_type_of_type env c = 
   let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
-
+*)
 (* Typing of several terms. *)
 
 let safe_machine_l env cl =
@@ -281,7 +282,7 @@ let add_constant_with_value sp body typ env =
 	    error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
   in
   let ids = 
-    Idset.union (global_vars_set body) (global_vars_set ty.body)
+    Idset.union (global_vars_set body) (global_vars_set (body_of_type ty))
   in
   let cb = { 
     const_kind = kind_of_path sp;
@@ -331,76 +332,84 @@ let add_parameter sp t env =
 
 (* Insertion of inductive types. *)
 
-(* [for_all_prods p env c] checks a boolean condition [p] on all types
-   appearing in products in front of [c]. The boolean condition [p] is a 
-   function taking a value of type [typed_type] as argument. *)
-
-let rec for_all_prods p env c =
-  match whd_betadeltaiota env Evd.empty c with
-    | DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) -> 
-	(p (make_typed t s)) &&
-	(let ty = { body = t; typ = s } in
-	 let env' = Environ.push_rel (name,ty) env in
-	 for_all_prods p env' c)
-    | DOP2(Prod, b, DLAM(name,c)) -> 
-	let (jb,cst) = unsafe_machine env b in
-	let var = assumption_of_judgment env Evd.empty jb in
-	(p var) &&
-	(let env' = Environ.push_rel (name,var) (add_constraints cst env) in
-	 for_all_prods p env' c)
-    | _ -> true
-
-let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c
-
-let enforce_type_constructor env univ j cst =
-  match whd_betadeltaiota env Evd.empty j.uj_type with
-    | DOP0 (Sort (Type uc)) -> 
-	Constraint.add (univ,Geq,uc) cst
-    | _ -> error "Type of Constructor not well-formed"
-
-let type_one_constructor env_ar nparams ar c =
-  let (params,dc) = mind_extract_params nparams c in
-  let env_par = push_rels params env_ar in
-  let (jc,cst) = safe_machine env_par dc in
-  let cst' = match sort_of_arity env_ar ar with
-    | Type u -> enforce_type_constructor env_par u jc cst
-    | Prop _ -> cst
-  in
-  let (j,cst'') = safe_machine env_ar c in
-  let issmall = is_small_type env_par dc in
-  ((issmall,j), Constraint.union cst' cst'')
-
-let logic_constr env c =
-  for_all_prods (fun t -> not (is_info_type env Evd.empty t)) env c
-
-let logic_arity env c =
-  for_all_prods 
-    (fun t -> 
-       (not (is_info_type env Evd.empty t)) or (is_small_type env t.body)) 
-    env c
-
-let is_unit env_par nparams ar spec =
-  match decomp_all_DLAMV_name spec with
-    | (_,[|c|]) ->
-	(let (_,a) = mind_extract_params nparams ar in 
-	 logic_arity env_par ar) &&
-	(let (_,c') = mind_extract_params nparams c in 
-	 logic_constr env_par c')
-    | _ -> false
+(* Only the case where at least s1 or s2 is a [Type] is taken into account *)
+let max_universe (s1,cst1) (s2,cst2) g =
+  match s1,s2 with
+    | Type u1, Type u2 ->
+	let (u12,cst) = sup u1 u2 g in
+	Type u12, Constraint.union cst (Constraint.union cst1 cst2)
+    | Type u1, _  -> s1, cst1
+    | _, _ -> s2, cst2
+
+(* This (re)computes informations relevant to extraction and the sort of
+   an arity or type constructor *)
+
+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 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 smax',cst' = max_universe (s1,cst1) (smax,cst) (universes env) in
+	let logic = not (is_info_type env Evd.empty var) in
+	let small = is_small s1 in
+	((logic,small) :: infos, smax', cst')
+    | IsCast (c,t) -> infos_and_sort env c
+    | _ ->
+	([],prop (* = neutral element of max_universe *),Constraint.empty)
+
+(* [infos] is a sequence of pair [islogic,issmall] for each type in
+   the product of a constructor or arity *)
+
+let is_small infos = List.for_all (fun (logic,small) -> small) infos
+let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
+let is_logic_arity infos =
+  List.for_all (fun (logic,small) -> logic || small) infos
+
+let is_unit arinfos constrsinfos =
+  match constrsinfos with  (* One info = One constructor *)
+   | [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
+   | _ -> false
+
+let small_unit constrsinfos (env_par,nparams,ar) =
+  let issmall = List.for_all is_small constrsinfos in
+  let (arinfos,_,_) =
+    let (_,a) = mind_extract_params nparams ar in infos_and_sort env_par a in
+  let isunit = is_unit arinfos constrsinfos in
+  issmall, isunit
+
+(* [smax] is the max of the sorts of the products of the constructor type *)
+
+let enforce_type_constructor arsort smax cst =
+  match smax, arsort with
+    | Type uc, Type ua -> Constraint.add (ua,Geq,uc) cst
+    | _,_ -> cst
+
+let type_one_constructor env_ar nparams arsort c =
+  let (infos,max,cst1) = 
+    let (params,dc) = mind_extract_params nparams c in
+    let env_par = push_rels params env_ar in
+    infos_and_sort env_par dc in
+  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)
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
   let (lna,vc) = decomp_all_DLAMV_name spec in
-  let ((issmall,jlc),cst') = 
+  let arsort = sort_of_arity env_ar ar in
+  let (constrsinfos,jlc,cst') = 
     List.fold_right
-      (fun c ((small,jl),cst) -> 
-	 let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in
-	 ((small && sm,jc::jl), Constraint.union cst cst'))
+      (fun c (infosl,jl,cst) -> 
+	 let (infos,jc,cst') = type_one_constructor env_ar nparams arsort c in
+	 (infos::infosl,jc::jl, Constraint.union cst cst'))
       (Array.to_list vc) 
-      ((true,[]),Constraint.empty)
+      ([],[],Constraint.empty)
   in
-  let castlc = List.map cast_of_judgment jlc in
+  let castlc = List.map incast_type jlc in
   let spec' = put_DLAMSV lna (Array.of_list castlc) in
-  let isunit = is_unit env_par nparams ar spec 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,spec'), cst')
 
@@ -431,7 +440,7 @@ let add_mind sp mie env =
     cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst
   in
   add_mind sp mib (add_constraints cst env)
-
+    
 let add_constraints = add_constraints
 
 let pop_vars idl env =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 07e95197c..e95aa2390 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -62,19 +62,20 @@ 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
+val safe_machine_type : safe_environment -> constr -> typed_type * constraints
 
 val fix_machine : safe_environment -> constr -> judgment * constraints
-val fix_machine_type : safe_environment -> constr -> typed_type
+val fix_machine_type : safe_environment -> constr -> typed_type * constraints
 
 val unsafe_machine : safe_environment -> constr -> judgment * constraints
-val unsafe_machine_type : safe_environment -> constr -> typed_type
+val unsafe_machine_type : safe_environment -> constr -> typed_type * constraints
 
 val type_of : safe_environment -> constr -> constr
 
+(*i obsolète 
 val type_of_type : safe_environment -> constr -> constr
-
 val unsafe_type_of : safe_environment -> constr -> constr
+i*)
 
 
 (*s Typing with information (extraction). *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 576a92182..3ed337847 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -68,6 +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
 
@@ -83,6 +84,21 @@ 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"
+(**)
+(*
+type typed_type = constr
+type typed_term = typed_type judge
+
+let make_typed t s = t
+
+let typed_app f tt = f tt
+
+let body_of_type ty = ty
+let level_of_type t = failwith "N'existe plus"
+
+let incast_type tty = tty
+let outcast_type x = x
+*)
 
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
@@ -196,11 +212,10 @@ let mkMutCaseA ci p c ac =
    Warning: as an invariant the ti are casted during the Fix formation;
    these casts are then used by destFix
 *)
-let in_fixcast {body=b; typ=s} = DOP2 (Cast, b, DOP0 (Sort s))
 
 (* Here, we assume the body already constructed *)
 let mkFixDlam recindxs i jtypsarray body =
-  let typsarray = Array.map in_fixcast jtypsarray in
+  let typsarray = Array.map incast_type jtypsarray in
   DOPN (Fix (recindxs,i),Array.append typsarray body)
 
 let mkFix recindxs i jtypsarray funnames bodies = 
@@ -229,7 +244,7 @@ let mkFix recindxs i jtypsarray funnames bodies =
 *)
 (* Here, we assume the body already constructed *)
 let mkCoFixDlam i jtypsarray body =
-  let typsarray = Array.map in_fixcast jtypsarray in
+  let typsarray = Array.map incast_type jtypsarray in
   DOPN ((CoFix i),(Array.append typsarray body))
 
 let mkCoFix i jtypsarray funnames bodies = 
@@ -491,7 +506,7 @@ let destCase = function
 *)
 
 let out_fixcast = function
-  | DOP2 (Cast, b, DOP0 (Sort s)) -> { body = b; typ = s }
+  | DOP2 (Cast, b, DOP0 (Sort s)) as c -> outcast_type c
   | _ -> anomaly "destFix: malformed recursive definition"
 
 let destGralFix a =
@@ -1368,8 +1383,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 d307e8dae..f3afa5e0a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -59,7 +59,7 @@ type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
 
-type typed_type = sorts judge
+type typed_type
 type typed_term = typed_type judge
 
 val make_typed : constr -> sorts -> typed_type
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 5c4b5e41c..c88711635 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -17,8 +17,8 @@ open Type_errors
 
 let make_judge v tj =
   { uj_val = v;
-    uj_type = tj.body;
-    uj_kind= DOP0 (Sort tj.typ) }
+    uj_type = body_of_type tj;
+    uj_kind= DOP0 (Sort (level_of_type tj)) }
 
 let j_val_only j = j.uj_val
 (* Faut-il caster ? *)
@@ -28,12 +28,13 @@ 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) -> { body = j.uj_type; typ = s }
+    | DOP0(Sort s) -> make_typed j.uj_type s
     | _ -> error_not_type CCI env j.uj_type
 
+
 let assumption_of_judgment env sigma j =
   match whd_betadeltaiota env sigma j.uj_type with
-    | DOP0(Sort s) -> { body = j.uj_val; typ = s }
+    | DOP0(Sort s) -> make_typed j.uj_val s
     | _ -> error_assumption CCI env j.uj_val
 
 (* Type of a de Bruijn index. *)
@@ -42,8 +43,8 @@ let relative env n =
   try
     let (_,typ) = lookup_rel n env in
     { uj_val  = Rel n;
-      uj_type = lift n typ.body;
-      uj_kind = DOP0 (Sort typ.typ) }
+      uj_type = lift n (body_of_type typ);
+      uj_kind = DOP0 (Sort (level_of_type typ)) }
   with Not_found -> 
     error_unbound_rel CCI env n
 
@@ -78,11 +79,7 @@ let check_hyps id env sigma hyps =
 
 (* Instantiation of terms on real arguments. *)
 
-let type_of_constant env sigma (sp,args) =
-  let cb = lookup_constant sp env in
-  let hyps = cb.const_hyps in
-  (* TODO: check args *)
-  instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
+let type_of_constant = Instantiate.constant_type
 
 (* Inductive types. *)
 
@@ -244,7 +241,7 @@ let is_correct_arity env sigma kelim (c,p) =
   in 
   srec
 
-let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =    
+let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =
   let mis = lookup_mind_specif mind env in
   let nparams = mis_nparams mis
   and kelim = mis_kelim mis
@@ -387,7 +384,8 @@ let sort_of_product_without_univ domsort rangsort =
 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 var.typ (destSort rngtyp) (universes env) in
+  let (s,cst) =
+    sort_of_product (level_of_type var) (destSort rngtyp) (universes env) in
   { uj_val = mkLambda name cvar (j_val j);
     uj_type = mkProd name cvar j.uj_type;
     uj_kind = mkSort s },
@@ -404,11 +402,11 @@ let gen_rel env sigma name var j =
   else
     match jtyp with
       | DOP0(Sort s) ->
-	  let (s',g) = sort_of_product var.typ s (universes env) in
+	  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 (mkCast var.body (mkSort var.typ)) (j_val_cast j);
+	      mkProd name (incast_type var) (j_val_cast j);
             uj_type = res_type;
             uj_kind = res_kind }, g'
       | _ -> 
@@ -967,7 +965,7 @@ let keep_hyps sign needed =
 	    (fun ((hyps,globs) as sofar) id a ->
                if Idset.mem id globs then
                  (add_sign (id,a) hyps, 
-		  Idset.union (global_vars_set a.body) globs)
+		  Idset.union (global_vars_set (body_of_type a)) globs)
                else 
 		 sofar) 
 	    (nil_sign,needed) sign))
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e526d82fb..541135442 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -55,6 +55,7 @@ val gen_rel :
   env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
     -> unsafe_judgment * constraints
 
+val sort_of_product : sorts -> sorts -> universes -> sorts * constraints
 val sort_of_product_without_univ : sorts -> sorts -> sorts
 
 val cast_rel :