machine: execute = typage avec univers

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

16 files changed, 940 insertions, 68 deletions

diff --git a/kernel/constant.mli b/kernel/constant.mli
index 4de51f8593..7f52f94d46 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -3,6 +3,7 @@
 
 open Names
 open Term
+open Sign
 
 type discharge_recipe
 
@@ -13,7 +14,8 @@ type recipe =
 type constant_body = {
   const_kind : path_kind;
   const_body : recipe ref option;
-  const_type : type_judgment;
+  const_type : typed_type;
+  const_hyps : context;
   mutable const_eval : ((int * constr) list * int * bool) option option;
 }
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index cc579f3509..c8e6b60060 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -7,7 +7,8 @@ open Univ
 open Term
 
 type 'a unsafe_env = {
-  context : context;
+  context : environment;
+  inf_context : environment option;
   sigma : 'a evar_map;
   metamap : (int * constr) list;
   constraints : universes
diff --git a/kernel/environ.mli b/kernel/environ.mli
index af2a131943..ec148edaa6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -14,17 +14,19 @@ val evar_map : 'a unsafe_env -> 'a evar_map
 val universes : 'a unsafe_env -> universes
 val metamap : 'a unsafe_env -> (int * constr) list
 
-val push_var : identifier * constr -> 'a unsafe_env -> 'a unsafe_env
-val push_rel : name * constr -> 'a unsafe_env -> 'a unsafe_env
+val push_var : identifier * typed_type -> 'a unsafe_env -> 'a unsafe_env
+val push_rel : name * typed_type -> 'a unsafe_env -> 'a unsafe_env
+val set_universes : universes -> 'a unsafe_env -> 'a unsafe_env
 
 val add_constant : constant_entry -> 'a unsafe_env -> 'a unsafe_env
 val add_mind : mind_entry -> 'a unsafe_env -> 'a unsafe_env
 
 val new_meta : unit -> int
 
-val lookup_var : identifier -> 'a unsafe_env -> constr
-val loopup_rel : int -> 'a unsafe_env -> name * constr
+val lookup_var : identifier -> 'a unsafe_env -> name * typed_type
+val lookup_rel : int -> 'a unsafe_env -> name * typed_type
 val lookup_constant : section_path -> 'a unsafe_env -> constant_entry
+val lookup_meta : int -> 'a unsafe_env -> constr
 
 val id_of_global : 'a unsafe_env -> sorts oper -> identifier
 val id_of_name_using_hdchar : 'a unsafe_env -> constr -> name -> identifier
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 77351ab9b7..5b870d87af 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -12,11 +12,10 @@ type evar_body =
     EVAR_EMPTY | EVAR_DEFINED of constr
 
 type 'a evar_info = {
-  concl : constr;            (* the type of the evar ...          *)
-  hyps  : context;           (* ... under a certain signature     *)
-  body  : evar_body;         (* its definition                    *) 
-  info  : 'a option          (* any other necessary information   *)
-}         
+  evar_concl : typed_type;        (* the type of the evar ...          *)
+  evar_hyps  : context;           (* ... under a certain signature     *)
+  evar_body  : evar_body;         (* its definition                    *) 
+  evar_info  : 'a option }        (* any other necessary information   *)
 
 type 'a evar_map = 'a evar_info Spmap.t
 
@@ -34,31 +33,32 @@ let add_with_info evd sp newinfo =
 
 let add_noinfo evd sp sign typ = 
   let newinfo = 
-    { concl = typ;
-      hyps  = sign;
-      body  = EVAR_EMPTY;
-      info  = None}
+    { evar_concl = typ;
+      evar_hyps  = sign;
+      evar_body  = EVAR_EMPTY;
+      evar_info  = None}
   in 
   Spmap.add sp newinfo evd
 
 let define evd sp body = 
- let oldinfo = map evd sp in
- let newinfo =
-   { concl = oldinfo.concl;
-     hyps  = oldinfo.hyps;
-     body  = EVAR_DEFINED body;
-     info  = oldinfo.info} 
- in
- match oldinfo.body with
-   | EVAR_EMPTY -> Spmap.add sp newinfo evd
-   | _ -> anomaly "cannot define an isevar twice"
+  let oldinfo = map evd sp in
+  let newinfo =
+    { evar_concl = oldinfo.evar_concl;
+      evar_hyps  = oldinfo.evar_hyps;
+      evar_body  = EVAR_DEFINED body;
+      evar_info  = oldinfo.evar_info} 
+  in
+  match oldinfo.evar_body with
+    | EVAR_EMPTY -> Spmap.add sp newinfo evd
+    | _ -> anomaly "cannot define an isevar twice"
 
 (* The list of non-instantiated existential declarations *)
 
 let non_instantiated sigma = 
-    let listsp = toList sigma in
-    List.fold_left 
-        (fun l ((sp,evd) as d) -> if evd.body = EVAR_EMPTY then (d::l) else l)
-        [] listsp
-
+  let listsp = toList sigma in
+  List.fold_left 
+    (fun l ((sp,evd) as d) -> 
+       if evd.evar_body = EVAR_EMPTY then (d::l) else l)
+    [] listsp
+    
 let is_evar sigma sp = in_dom sigma sp
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 8ed6babc08..bdbd759156 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -19,10 +19,10 @@ type evar_body =
   | EVAR_DEFINED of constr
 
 type 'a evar_info = {
-  concl : constr;
-  hyps  : context;
-  body  : evar_body;
-  info  : 'a option }
+  evar_concl : typed_type;
+  evar_hyps  : context;
+  evar_body  : evar_body;
+  evar_info  : 'a option }
 
 type 'a evar_map
 
@@ -36,7 +36,7 @@ val toList : 'a evar_map -> (section_path * 'a evar_info) list
 val mt_evd : 'a evar_map
 val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
 val add_noinfo : 
-  'a evar_map -> section_path -> context -> constr -> 'a evar_map
+  'a evar_map -> section_path -> context -> typed_type -> 'a evar_map
 
 val define : 'a evar_map -> section_path -> constr -> 'a evar_map
 
diff --git a/kernel/himsg.mli b/kernel/himsg.mli
new file mode 100644
index 0000000000..f51f427604
--- /dev/null
+++ b/kernel/himsg.mli
@@ -0,0 +1,14 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Sign
+open Environ
+(*i*)
+
+val error_unbound_rel : path_kind -> 'a unsafe_env -> int -> 'b
+
+val error_cant_execute : path_kind -> 'a unsafe_env -> constr -> 'b
diff --git a/kernel/mach.ml b/kernel/mach.ml
new file mode 100644
index 0000000000..7501b45b7b
--- /dev/null
+++ b/kernel/mach.ml
@@ -0,0 +1,726 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Univ
+open Generic
+open Term
+open Himsg
+open Reduction
+open Environ
+open Machops
+
+(* Fonctions temporaires pour relier la forme castée de la forme jugement *)
+let tjudge_of_cast env = function
+  | DOP2 (Cast, b, t) ->
+      (match whd_betadeltaiota env t with
+	 | DOP0 (Sort s) -> {body=b; typ=s}
+	 | DOP2 (Cast, b',t') -> anomaly "Supercast (tjudge_of_cast) [Mach]"
+	 | _ -> anomaly "Not a type (tjudge_of_cast) [Mach]")
+  | _ -> anomaly "Not casted (tjudge_of_cast)"
+	
+let tjudge_of_judge env j =
+  { body = j.uj_val;
+    typ = match whd_betadeltaiota env j.uj_type with
+      (* Nécessaire pour ZFC *)
+      | DOP0 (Sort s) -> s
+      | DOP0 Implicit -> anomaly "Tiens, un implicit"
+      | _ -> anomaly "Not a type (tjudge_ofjudge)" }
+
+let vect_lift = Array.mapi lift
+let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+
+(* Ce type est introduit pour rendre un peu plus lisibles les appels a la
+   machine de typage.
+
+   nofix indique si on autorise les points fixes generaux (recarg < 0)
+     comme Acc_rec.fw
+   nocheck devrait indiquer que l'on cherche juste a calculer le type, sans
+     faire toutes les verifications (par exemple, pour l'application, on
+     n'a pas a calculer le type des arguments, et les Cast devraient etre
+     utilises). Pour l'instant, on fait trop de verifications
+   noverify indique qu'il ne faut pas verifier si les contextes sont bien
+     castes
+   Rem: is_ass a disparu; les fonctions attendant un type retourne
+        maintenant un "type_judgement" et non un "judgement" complet
+ *)
+
+type 'a mach_flags = {
+  nofix : bool;
+  nocheck : bool;
+  noverify : bool }
+
+(* WARNING: some destCast are not guarded.
+   Invariant: assumptions in env are casted (checked when noverify=false) *)
+let rec execute mf env cstr =
+  let u0 = universes env in
+  match kind_of_term cstr with
+    | IsMeta n ->
+       	let metaty =
+          try lookup_meta n env
+          with Not_found -> error "A variable remains non instanciated" 
+	in
+        (match kind_of_term metaty with
+           | IsCast (typ,kind) -> 
+	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind}, u0)
+           | _ ->
+	       let (jty,u1) = execute mf env metaty in
+	       let k = hnf_constr env jty.uj_type in
+	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1))
+	
+    | IsRel n -> 
+	(relative env n, u0)
+
+    | IsVar id -> 
+	(make_judge cstr (snd (lookup_var id env)), u0)
+	  
+    | IsAbst _ ->
+        if evaluable_abst env cstr then 
+	  execute mf env (abst_value env cstr)
+        else 
+	  error "Cannot typecheck an unevaluable abstraction"
+	      
+    | IsConst _ ->
+        (make_judge cstr (type_of_const env cstr), u0)
+	  
+    | IsMutInd _ ->
+	(make_judge cstr (type_of_mind env cstr), u0)
+	  
+    | IsMutConstruct _ -> 
+        (make_judge cstr (type_of_mconstr env cstr), u0)
+	  
+    | IsMutCase (_,p,c,lf) ->
+        let (cj,u1) = execute mf env c in
+	let env1 = set_universes u1 env in
+        let (pj,u2) = execute mf env1 p in
+	let env2 = set_universes u2 env1 in
+        let (lfj,u3) = execute_array mf env2 lf in
+	let env3 = set_universes u3 env2 in
+        (type_of_case env3 pj cj lfj, u3)
+  
+    | IsFix (vn,i,lar,lfi,vdef) ->
+        if mf.nofix & array_exists (fun n -> n < 0) vn then
+          error "General Fixpoints not allowed";
+        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let fix = mkFix vn i larv lfi vdefv in
+        check_fix env fix;
+	(make_judge fix larv.(i), u1)
+	  
+    | IsCoFix (i,lar,lfi,vdef) ->
+        let (larv,vdefv,u1) = execute_fix mf env lar lfi vdef in
+        let cofix = mkCoFix i larv lfi vdefv in
+        check_cofix env cofix;
+	(make_judge cofix larv.(i), u1)
+	  
+    | IsSort (Prop c) -> 
+	(type_of_proposition c, u0)
+
+    | IsSort (Type u) ->
+	type_of_type u u0
+	  
+    | IsAppL a ->
+	let la = Array.length a in
+	if la = 0 then error_cant_execute CCI env cstr;
+	let hd = a.(0)
+	and tl = Array.to_list (Array.sub a 1 (la - 1)) in
+	let (j,u1) = execute mf env hd in
+	let env1 = set_universes u1 env in
+        let (jl,u2) = execute_list mf env1 tl in
+	let env2 = set_universes u2 env1 in
+	apply_rel_list env2 mf.nocheck jl j
+	    
+    | IsLambda (name,c1,c2) -> 
+        let (j,u1) = execute mf env c1 in
+        let var = assumption_of_judgement env j in
+	let env1 = push_rel (name,var) (set_universes u1 env) in
+        let (j',u2) = execute mf env1 c2 in 
+	let env2 = set_universes u2 env1 in
+        (abs_rel env2 name var j', u2)
+	  
+    | IsProd (name,c1,c2) ->
+        let (j,u1) = execute mf env c1 in
+        let var = assumption_of_judgement env j in
+	let env1 = push_rel (name,var) (set_universes u1 env) in
+        let (j',u2) = execute mf env1 c2 in
+	let env2 = set_universes u2 env1 in
+        (gen_rel env2 name var j', u2)
+	  
+    | IsCast (c,t) ->
+        let (cj,u1) = execute mf env c in
+	let env1 = set_universes u1 env in
+        let (tj,u2) = execute mf env1 t in
+	let env2 = set_universes u2 env1 in
+        (cast_rel env2 cj tj, u2)
+	  
+      | _ -> error_cant_execute CCI env cstr
+	  
+and execute_fix mf env lar lfi vdef =
+  let (larj,u1) = execute_array mf env lar in
+  let env1 = set_universes u1 env in
+  let lara = Array.map (assumption_of_judgement env1) larj in
+  let nlara = 
+    List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
+  let env2 = 
+    List.fold_left (fun env nvar -> push_rel nvar env) env1 nlara in
+  let (vdefj,u2) = execute_array mf env2 vdef in
+  let env3 = set_universes u2 env2 in
+  let vdefv = Array.map j_val_only vdefj in
+  let u3 = type_fixpoint env3 lfi lara vdefj in
+  (lara,vdefv,u3)
+
+and execute_array mf env v =
+  let (jl,u1) = execute_list mf env (Array.to_list v) in
+  (Array.of_list jl, u1)
+
+and execute_list mf env = function
+  | [] -> ([], universes env)
+  | c::r -> 
+      let (j,u') = execute mf env c in 
+      let (jr,u'') = execute_list mf (set_universes u' env) r in
+      (j::jr, u'')
+
+
+(** ICI **)
+
+let flag_fmachine mf env constr = 
+  if not mf.noverify then verify_wf_env env; 
+  exemeta_rec mf env constr
+
+let flag_fmachine_type mf env constr = 
+  if not mf.noverify then verify_wf_env env; 
+  let j = exemeta_rec mf env constr in
+  type_judgement mf.sigma env j
+
+
+(* This function castifies the term (nocheck=true).
+ * It must be applied to well-formed terms.
+ * Casts are all removed before re-computing them. This avoids casting
+ * Casts, which leads to terrible inefficiencies. *)
+let cast_fmachine (sigma,metamap) env t =
+  flag_fmachine
+    { nofix = true;
+      nocheck = true;
+      noverify = true;
+      sigma = sigma;
+      metamap = metamap}
+    env (strip_all_casts t)
+    
+(* core_fmachine* :
+   No general fixpoint allowed; checks that environments are casted *)
+let core_fmachine nocheck (sigma,metamap) env constr = 
+  flag_fmachine
+    { nofix = true;
+      nocheck = nocheck;
+      noverify = false;
+      sigma = sigma;
+      metamap = metamap}
+    env
+    constr
+
+let core_fmachine_type nocheck (sigma,metamap) env constr = 
+  flag_fmachine_type
+    { nofix = true;
+     nocheck = nocheck;
+     noverify = false;
+     sigma = sigma;
+     metamap = metamap}
+    env
+    constr
+
+(* WITHOUT INFORMATION *)
+let fmachine nocheck sig_meta sign constr =
+  let j = core_fmachine nocheck sig_meta sign constr in
+  { uj_val = strip_all_casts j.uj_val;
+    uj_type = strip_all_casts j.uj_type;
+    uj_kind = j.uj_kind }
+
+let fmachine_type nocheck sig_meta sign constr =
+  let j = core_fmachine_type nocheck sig_meta sign constr in
+  type_app strip_all_casts j
+    
+    
+let fexemeta_type sigma metamap env c = 
+  fmachine_type true (sigma,metamap) env c
+
+let execute_rec_type sigma env c = 
+  fmachine_type false (sigma,[]) env c
+
+let fexecute_type sigma sign c = 
+  fmachine_type false (sigma,[]) (gLOB sign) c
+
+let fexemeta sigma metamap env c = 
+  fmachine true (sigma,metamap) env c
+
+let execute_rec sigma env c = 
+  fmachine false (sigma,[]) env c
+
+let fexecute sigma sign c = 
+  fmachine false (sigma,[]) (gLOB sign) c
+
+let type_of_rel_type sigma env c = 
+  try 
+    let j = core_fmachine_type false (sigma,[]) env c in
+    DOP0 (Sort j.typ)
+  with Invalid_argument s -> 
+    error ("Invalid arg " ^ s)
+
+let type_of_rel sigma env c = 
+  try 
+    let j = core_fmachine false (sigma,[]) env c in
+    nf_betaiota j.uj_type
+  with Invalid_argument s -> 
+    error ("Invalid arg " ^ s)
+
+let type_of sigma sign c = type_of_rel sigma (gLOB sign) c
+
+let type_of_type sigma sign c = type_of_rel_type sigma (gLOB sign) c
+
+
+(* Allows general fixpoints to appear in the term *)
+let fixfexemeta sigma metamap env constr =
+  let j =
+    flag_fmachine
+      { nofix = false;
+       nocheck = true;
+       noverify = false;
+       sigma = sigma;
+       metamap = metamap }
+      env
+      constr
+  in 
+  { uj_val = strip_all_casts j.uj_val;
+    uj_type = strip_all_casts j.uj_type;
+    uj_kind = j.uj_kind }
+
+let unsafe_type_of sigma env c = 
+  try 
+    nf_betaiota
+      (flag_fmachine
+	 { nofix = false;
+           nocheck = true;
+           noverify = true;
+	   sigma = sigma;
+           metamap = [] }
+	 env
+	 c).uj_type
+  with Invalid_argument s -> 
+    error ("Invalid arg " ^ s)
+      
+let compute_type sigma env c = 
+  match c with
+    | DOP2(Cast,_,t) -> nf_betaiota t 
+    | _ -> unsafe_type_of sigma env c
+
+(* Les fonctions suivantes sont pour l'inversion (inv.ml, gelim.ml, leminv.ml):
+   sign_of_sign*
+   env_of_env*
+   castify_env*
+   castify_sign*
+
+   A uniformiser...
+ *)
+
+let sign_of_sign sigma sign =
+  sign_it
+    (fun id a sign ->
+       match a with
+           DOP2(Cast,t,DOP0 (Sort s)) -> add_sign (id,make_type t s) sign
+         | _ -> let j = fexecute sigma sign a in
+             (add_sign (id,assumption_of_judgement sigma (gLOB sign) j) sign))
+    sign nil_sign
+
+
+(*
+let env_of_env1 is_ass sigma env =
+  dbenv_it
+    (fun na a env ->
+       match a with
+           DOP2(Cast,_,_) -> add_rel (na,a) env
+         | _ -> let j = execute_rec1 is_ass sigma env a in
+             add_rel (na,assumption_of_judgement sigma env j) env)
+    env (gLOB(get_globals env))
+
+*)
+let env_of_env sigma env =
+  dbenv_it
+    (fun na a env ->
+       let j = execute_rec sigma env a in
+         add_rel (na,assumption_of_judgement sigma env j) env)
+    env (gLOB(get_globals env))
+
+
+let castify_sign sigma sign = sign_of_sign sigma sign
+
+let castify_env sigma env =
+  let sign = (* castify_sign sigma *) (get_globals env)
+  in env_of_env sigma (ENVIRON(sign,get_rels env))
+
+
+(* Fin fonctions pour l'inversion *)
+
+(**)
+
+let implicit_judgment = {body=mkImplicit;typ=implicit_sort}
+
+let add_inf_rel (na,inf) env =
+  match inf with
+      Logic -> add_rel (na,implicit_judgment) env
+    | Inf j -> add_rel (na,tjudge_of_judge j) env
+
+
+let fw_mutind sigma fenv k =
+  let (sp,x,args) = destMutInd k in
+  let mis = mind_specif_of_mind k in
+    match mis_singl mis with 
+	Some a -> Some (a,true)
+      | None ->
+	  if is_info_cast_type sigma (mis_arity mis) then
+	    let infK =
+              global_reference fenv (fwsp_of sp) (id_of_global (MutInd (sp,x)))
+	    in Some (infK,false)
+	  else None
+
+let inf_of_mind sigma fenv mind = 
+  try
+    match fw_mutind sigma fenv mind with
+        Some (infK,singl) -> Inf(cast_fmachine (sigma,[]) fenv infK)
+      | None -> Logic
+  with
+      Not_found | Failure _ -> 
+	anomaly "cannot convert an inductive to an finductive"
+
+let inf_mconstructor (sigma,metamap) fenv k = 
+  let (sp,x,i,cl) = destMutConstruct k in
+  let mind = mkMutInd sp x cl in 
+    (match fw_mutind sigma fenv mind with
+         None -> Logic
+       | Some(infi,singl) ->
+	   (match mind_lamexp mind with
+	      | Some clamexp ->
+		  if singl
+		  then Inf(cast_fmachine (sigma,[]) fenv clamexp)
+		  else
+		    let (infsp, infx, infcl) = destMutInd infi in
+		    let infmconstructor = mkMutConstruct infsp infx i infcl in
+		    let infval = subst1 infmconstructor clamexp in
+		      Inf (cast_fmachine (sigma,fst metamap) fenv infval)
+	      | _ -> assert false))
+
+
+exception DefinedExtraction
+
+(* when c is an evaluable constant with an extraction which 
+   contains an implicit, gives the value of the c constant
+   otherwise raise DefinedExtraction
+*)
+
+let value_implicit_const sigma c cinf = 
+  match c with DOPN(Const(_),_) -> 
+    if evaluable_const sigma c then 
+      let cv = const_value sigma cinf in 
+	if is_implicit cv (* or contains_implicit sigma cv *)
+	then const_value sigma c 
+	else raise DefinedExtraction
+    else raise DefinedExtraction
+    | _ -> raise DefinedExtraction
+
+let unsafe_infmachine (sigma,metamap) env fenv c = 
+  let rec infexec env fenv cstr = match cstr with
+       DOP2(Cast,c,DOP0(Sort(Prop(Null)))) -> Logic
+    |  DOP2(Cast,c,DOP2(Cast,_,DOP0(Sort(Prop(Null))))) -> Logic
+    |  DOP2(Cast,c,_) -> infexec env fenv c
+    |  DOP0(Meta n) ->
+         (match List.assoc n (snd metamap) with
+             Logic -> Logic
+           | Inf j -> Inf{uj_val=DOP0(Meta n);
+                          uj_type=j.uj_val;
+                          uj_kind = hnf_constr sigma j.uj_type})
+
+    | Rel n ->
+        inf_rel fenv
+          (contents_of_type sigma (snd (lookup_rel n env))) n
+
+    | VAR str ->
+        inf_var fenv
+          (contents_of_type sigma (snd(lookup_glob str env))) str
+
+    | DOPN(Const _,_) -> inf_of_const sigma (env,fenv) cstr
+
+    | DOPN(Abst _,_) ->
+        if evaluable_abst cstr then infexec env fenv (abst_value cstr)
+        else error "cannot extract from an unevaluable abstraction"
+
+    | DOP0(Sort s) -> inf_sort s
+
+    | DOPN(AppL,tl) ->
+        let c1 =  (hd_vect tl)
+        and cl = tl_vect tl in
+          let funinf = infexec env fenv c1 in
+            (match funinf with Logic -> Logic
+	      | Inf(j) -> let cinf = j.uj_val in
+             (* try to expand constants corresponding 
+		    to non extractable terms *)
+	      (try if is_extraction_expanded() then 
+		 let valcte = value_implicit_const sigma c1 cinf 
+		 in infexec env fenv (whd_betaiota (appvect(valcte,cl))) 
+	       else raise DefinedExtraction
+               with DefinedExtraction -> 
+		 let argsinf = Array.map (infexec env fenv) cl
+		 in it_vect inf_apply funinf argsinf))
+
+    | DOP2(Lambda,c1,DLAM(name,c2)) ->
+        let varinf = infexec env fenv c1 in
+        let bodyinf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
+                        (add_inf_rel (name,varinf) fenv) c2
+        in inf_abs_rel name bodyinf varinf
+
+    | DOP2(Prod,c1,DLAM(name,c2)) ->
+        let c1inf = infexec env fenv c1 in
+        let c2inf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
+                      (add_inf_rel (name,c1inf) fenv) c2
+        in inf_gen_rel name c2inf c1inf
+
+    | DOPN(MutInd _,_) -> inf_of_mind sigma fenv cstr
+
+    | DOPN(MutConstruct _,_) ->
+        inf_mconstructor (sigma,metamap) fenv cstr
+
+    | DOPN(Fix(vn,i),cl) ->
+        let lar = Array.sub cl 0 ((Array.length cl) - 1) in
+        let inflar = Array.map (infexec env fenv) lar in
+        let infAi = inflar.(i) in 
+          (match infAi with 
+              Logic   -> Logic 
+            | Inf aij ->
+                let (lfi,ldefs) = decomp_all_DLAMV_name (last_vect cl) in
+                let (new_env,new_fenv) =
+                  it_vect2
+                    (fun (ne,nfe) fk ak -> 
+                       (add_rel (fk,tjudge_of_cast sigma ak) ne,
+                        let infAk = infexec ne nfe ak
+                        in (add_inf_rel (fk,infAk) nfe)))
+                    (env,fenv)
+                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
+(* a special function to localize the recursive index in the extracted term *)
+                let rec exec_def ne nfe n def = 
+                  (match hnf_constr sigma def with 
+                      DOP2(Lambda,c1,DLAM(name,c2)) ->
+                        let varinf = infexec ne nfe c1 in
+                        let ne' = (add_rel (name,tjudge_of_cast sigma c1) ne) 
+                        and nfe' = add_inf_rel (name,varinf) nfe in
+                          if n = 0 then
+                            let infc2 = infexec ne' nfe' c2 
+                            in let infdef = inf_abs_rel name infc2 varinf
+                               and index =
+                                 if varinf = Logic then -1
+                        (* the recursive call was on a non-informative term *) 
+                                 else 0 in (infdef,index)
+                          else
+                            let bodyinf,countl = 
+                              exec_def (add_rel (name,tjudge_of_cast sigma c1) ne) 
+                                (add_inf_rel (name,varinf) nfe) (n-1) c2 in
+                            let (infabs,abs) =
+                              inf_abs_rel_count name bodyinf varinf
+                            in (infabs,
+                                if abs = ERASE then countl
+                                else if countl<0 then countl-1
+                                else countl+1)
+                    | _ -> anomaly "exec_def : should be a lambda") in
+                let infdefs_ind =
+                  map2_vect (exec_def new_env new_fenv) vn ldefs
+                in inf_fix sigma i aij.uj_type lfi inflar infdefs_ind)
+
+    | DOPN(CoFix i,cl) ->
+        let lar    = Array.sub cl 0 ((Array.length cl) - 1) in 
+        let inflar = Array.map (infexec env fenv) lar in
+        let infAi  = inflar.(i) in
+          (match infAi with 
+              Logic   -> Logic 
+            | Inf aij -> 
+                let lfi,ldefs = decomp_all_DLAMV_name (last_vect cl) in 
+                let (new_env,new_fenv) = 
+                  it_vect2 (fun (ne,nfe) fk ak -> 
+                              (add_rel (fk,tjudge_of_cast sigma ak) ne, 
+                               let infAk = infexec ne nfe ak
+                               in (add_inf_rel (fk,infAk) nfe)))
+                    (env,fenv) 
+                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
+                                   
+                let infdefs = Array.map (infexec new_env new_fenv) ldefs 
+                in  inf_cofix sigma i aij.uj_type lfi inflar infdefs)
+
+    | DOPN(MutCase _,_) ->
+        let (ci,p,c,lf) = destCase cstr in
+        let pinf = infexec env fenv p in 
+          (match pinf with
+              Logic  -> Logic 
+            | Inf pj -> 
+		if is_extraction_expanded() then 
+		  let (d,l) = whd_betadeltaiota_stack sigma c [] in 
+                 (match d with (DOPN(MutConstruct(_,_),_)) ->
+		    let cstr' = 
+		      DOPN(MutCase(ci),Array.append [|p;applist(d,l)|] lf)
+		    in infexec env fenv (whd_betaiota cstr')
+		    | _ -> 
+                  let cinf = infexec env fenv c
+                  and lfinf = Array.map (infexec env fenv) lf
+                  in inf_mutcase fenv sigma pj ci cinf lfinf
+		 )
+               else let cinf = infexec env fenv c
+                  and lfinf = Array.map (infexec env fenv) lf
+                  in inf_mutcase fenv sigma pj ci cinf lfinf)
+	 
+    | _ -> error "Cannot extract information"
+  in infexec env fenv c
+
+
+let core_infmachine meta env fenv c =
+  try unsafe_infmachine meta env fenv c
+  with (UserError _ | Failure _) -> Logic
+
+(* WITH INFORMATION *)
+(* does not check anymore that extracted terms are well-formed *)
+let judgement_infmachine meta env fenv c ct = 
+  try
+    match unsafe_infmachine meta env fenv c with
+        Inf infj ->
+          let inftyp =
+            try unsafe_infmachine meta env fenv ct
+            with (UserError _ | Failure _) ->
+              (warning "Failed to extract in type"; Logic)
+          in (match inftyp with
+                  Inf infjt ->
+                    Inf{uj_val=infj.uj_val;
+                        uj_type=infjt.uj_val;
+                        uj_kind=infj.uj_kind}
+                | Logic -> Inf infj)
+      | Logic -> Logic
+  with (UserError _ | Failure _) -> (warning "Failed to extract"; Logic)
+
+let infmachine_type nocheck (sigma,metamap) env fenv constr =
+  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
+  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
+  let t = core_fmachine_type nocheck (sigma,constr_metamap) env constr in
+  let inf = 
+    if is_info_type sigma t then (* Case the term is informative *)
+      let uniarc = get_uniarc () in
+      let infjt =
+        judgement_infmachine
+          (sigma,(constr_metamap,inf_metamap)) env fenv 
+	  t.body 
+	  (DOP0 (Sort t.typ)) in
+      let _ = set_uniarc uniarc in
+        infjt
+    else Logic
+
+  in hash_jpair_type
+       ({body = strip_all_casts t.body; typ = t.typ},
+        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
+                            uj_type = nf_beta j.uj_type;
+                            uj_kind = j.uj_kind }) inf))
+
+let infmachine nocheck (sigma,metamap) env fenv constr =
+  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
+  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
+  let j = core_fmachine nocheck (sigma,constr_metamap) env constr in
+  let inf = 
+    if is_info_judge sigma j then (* Case the term is informative *)
+      let uniarc = get_uniarc () in
+      let jt = cast_fmachine (sigma,constr_metamap) env j.uj_type in
+      let infjt =
+        judgement_infmachine
+          (sigma,(constr_metamap,inf_metamap)) env fenv j.uj_val jt.uj_val in
+      let _ = set_uniarc uniarc in
+        infjt
+    else Logic
+
+  in hash_jpair
+       ({uj_val = strip_all_casts j.uj_val;
+         uj_type = strip_all_casts j.uj_type;
+         uj_kind = j.uj_kind},
+        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
+                            uj_type = nf_beta j.uj_type;
+                            uj_kind = j.uj_kind }) inf))
+
+
+let jsign_of_sign sigma sign =
+  sign_it
+    (fun id a (sign,fsign) ->
+      let sign' = add_sign (id,a) sign in
+      let fsign' =
+        match infmachine_type true (sigma,[]) (gLOB sign) (gLOB fsign) a.body
+ 	with
+          (_,Logic) -> fsign
+        | (_,Inf ft) -> add_sign (id,tjudge_of_judge ft) fsign
+      in (sign',fsign'))
+    sign (([],[]),([],[]))
+
+
+let fsign_of_sign sigma sign = snd (jsign_of_sign sigma sign)
+
+let infexemeta_type sigma metamap (env,fenv) c =
+  infmachine_type true (sigma,metamap) env fenv c
+
+let infexecute_rec_type sigma (env,fenv) c =
+  infmachine_type false (sigma,[]) env fenv c
+
+let infexecute_type sigma (sign,fsign) c =
+  infmachine_type false (sigma,[]) (gLOB sign) (gLOB fsign) c
+
+let infexemeta sigma metamap (env,fenv) c =
+  infmachine true (sigma,metamap) env fenv c
+
+let infexecute_rec sigma (env,fenv) c =
+  infmachine false (sigma,[]) env fenv c
+
+let infexecute sigma (sign,fsign) c =
+  infmachine false (sigma,[]) (gLOB sign) (gLOB fsign) c
+
+(* A adapter pour les nouveaux env
+let fvar_type sigma (sign,fsign) v = 
+  let na = destVar v in
+  let varty = (snd(lookup_sign na sign))
+  in match (snd(infexemeta sigma [] (gLOB sign, gLOB fsign) varty)) with
+      Inf ft -> ft.uj_val
+    | Logic -> invalid_arg "Fvar with a non-informative type (1)!"
+
+*)
+
+(* MACHINE WITH UNIVERSES *)
+(* Il vaudrait mieux typer dans le graphe d'univers de Constraintab,
+   recuperer le graphe local, et restaurer l'acien graphe global *)
+
+let whd_instuni = function
+    DOP0(Sort(Type(u))) ->
+      let u = (if u = dummy_univ then new_univ() else u)
+      in DOP0(Sort(Type(u)))
+  | c -> c
+
+(* Instantiate universes: replace all dummy_univ by fresh universes.
+   This is already done by the machine.
+   Indtypes instantiates the universes itself, because in the case of
+   large constructor, additionnal constraints must be considered. *)
+let instantiate_universes c = strong whd_instuni c
+
+
+(* sp est le nom de la constante pour laquelle il faut que c soit bien type.
+   Cela sert a eviter un clash entre le noms d'univers de 2 modules compiles
+   independamment.
+   Au lieu de sp, Lib.cwd() serait peut-etre suffisant.
+   Cela eviterai de donner un section-path quand on veut typer. *)
+let fexecute_type_with_univ sigma sign sp c =
+  with_universes (fexecute_type sigma sign) (sp,initial_universes,c) 
+
+
+let fexecute_with_univ sigma sign sp c =
+  with_universes (fexecute sigma sign) (sp,initial_universes,c) 
+
+
+let infexecute_type_with_univ sigma psign sp c =
+  with_universes (infexecute_type sigma psign) (sp,initial_universes,c) 
+
+
+let infexecute_with_univ sigma psign sp c =
+  with_universes (infexecute sigma psign) (sp,initial_universes,c) 
diff --git a/kernel/mach.mli b/kernel/mach.mli
new file mode 100644
index 0000000000..701c2a58f8
--- /dev/null
+++ b/kernel/mach.mli
@@ -0,0 +1,48 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Univ
+open Environ
+open Machops
+(*i*)
+
+(*s Machine without information. *)
+
+val fexecute_type : 'a unsafe_env -> constr -> typed_type
+val fexecute : 'a unsafe_env -> constr -> unsafe_judgment
+
+val execute_rec_type : 'a unsafe_env -> constr -> typed_type
+val execute_rec : 'a unsafe_env -> constr -> unsafe_judgment
+
+val type_of : 'a unsafe_env -> constr -> constr
+val type_of_type : 'a unsafe_env -> constr -> constr
+
+val type_of_rel : 'a unsafe_env -> constr -> constr
+
+val unsafe_type_of : 'a unsafe_env -> constr -> constr
+
+val fexemeta_type : 'a unsafe_env -> constr -> typed_type
+val fexemeta : 'a unsafe_env -> constr -> unsafe_judgment
+
+val core_fmachine_type : bool -> 'a unsafe_env -> constr -> typed_type
+val core_fmachine : bool -> 'a unsafe_env -> constr -> unsafe_judgment
+
+
+(*s Machine with information. *)
+
+val infexemeta : 
+  'a unsafe_env -> constr -> unsafe_judgment * information * universes
+
+val infexecute_type : 
+  'a unsafe_env -> constr -> typed_type * information * universes
+
+val infexecute : 
+  'a unsafe_env -> constr -> unsafe_judgment * information * universes
+
+val inf_env_of_env : 'a unsafe_env -> 'a unsafe_env
+
+val core_infmachine : 'a unsafe_env -> constr -> information
diff --git a/kernel/machops.mli b/kernel/machops.mli
new file mode 100644
index 0000000000..c59d3344d8
--- /dev/null
+++ b/kernel/machops.mli
@@ -0,0 +1,63 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Univ
+open Term
+open Environ
+(*i*)
+
+(* Typing judgments. *)
+
+type unsafe_judgment = { 
+  uj_val : constr;
+  uj_type : constr;
+  uj_kind : constr }
+
+type information = Logic | Inf of unsafe_judgment
+
+val make_judge : constr -> typed_type -> unsafe_judgment
+
+val j_val_only : unsafe_judgment -> constr
+
+
+(* Base operations of the typing machine. *)
+
+val relative : 'a unsafe_env -> int -> unsafe_judgment
+
+val type_of_const : 'a unsafe_env -> constr -> typed_type
+
+val type_of_mind : 'a unsafe_env -> constr -> typed_type
+
+val type_of_mconstr : 'a unsafe_env -> constr -> typed_type
+
+val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment 
+  -> unsafe_judgment array -> unsafe_judgment
+
+val type_of_proposition : contents -> unsafe_judgment
+
+val type_of_type : universe -> universes -> unsafe_judgment * universes
+
+val assumption_of_judgement : 'a unsafe_env -> unsafe_judgment -> typed_type
+
+val abs_rel : 
+  'a unsafe_env -> name -> typed_type -> unsafe_judgment -> unsafe_judgment
+
+val gen_rel :
+  'a unsafe_env -> name -> typed_type -> unsafe_judgment -> unsafe_judgment
+
+val cast_rel : 
+  'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+
+val apply_rel_list : 
+  'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment
+    -> unsafe_judgment * universes
+
+val check_fix : 'a unsafe_env -> constr -> unit
+val check_cofix : 'a unsafe_env -> constr -> unit
+
+val type_fixpoint : 'a unsafe_env -> name list -> typed_type array 
+    -> unsafe_judgment array -> universes
+
+
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5636bbbc81..d02d95277e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -745,6 +745,8 @@ let convert_of_constraint f u =
     | Consistent u' -> Convertible u'
     | Inconsistent -> NotConvertible
 
+type conversion_test = universes -> conversion_result
+
 let convert_of_bool b u =
   if b then Convertible u else NotConvertible
 
@@ -761,7 +763,7 @@ let convert_or f1 f2 u =
     | NotConvertible -> f2 u
     | c -> c
 
-let forall2_conv f v1 v2 u =
+let convert_forall2 f v1 v2 u =
   array_fold_left2 
     (fun a x y -> match a with
        | NotConvertible -> NotConvertible
@@ -802,16 +804,16 @@ and eqappr cv_pb infos appr1 appr2 =
 	  
     | (FVAR x1, FVAR x2) ->
 	bool_and_convert (x1=x2)
-	  (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+	  (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
     | (FRel n, FRel m) ->
         bool_and_convert 
 	  (reloc_rel n el1 = reloc_rel m el2)
-          (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+          (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
     | (FOP0(Meta(n)), FOP0(Meta(m))) ->
         bool_and_convert (n=m) 
-	  (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+	  (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
     | (FOP0 Implicit, FOP0 Implicit) ->
         convert_of_bool (Array.length v1 = 0 & Array.length v2 = 0)
@@ -822,8 +824,8 @@ and eqappr cv_pb infos appr1 appr2 =
 	  (* try first intensional equality *)
 	  (bool_and_convert (sp1 == sp2 or sp1 = sp2)
 	     (convert_and
-		(forall2_conv (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-		(forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (match search_frozen_cst infos (Const sp2) al2 with
              | Some def2 -> 
@@ -838,8 +840,8 @@ and eqappr cv_pb infos appr1 appr2 =
 	  (* try first intensional equality *)
           (bool_and_convert  (sp1 = sp2)
 	     (convert_and
-		(forall2_conv (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-		(forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (match search_frozen_cst infos (Abst sp2) al2 with
              | Some def2 -> 
@@ -885,14 +887,14 @@ and eqappr cv_pb infos appr1 appr2 =
 
     | (FOPN(MutCase _,cl1), FOPN(MutCase _,cl2)) ->
         convert_and
-	  (forall2_conv (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
-          (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+	  (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
+          (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
      | (FOPN(op1,cl1), FOPN(op2,cl2)) ->
 	 bool_and_convert (op1 = op2)
 	   (convert_and
-              (forall2_conv (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
-              (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
+              (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
+              (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
 
      (* binders *)
      | (FLAM(_,c1,_,_), FLAM(_,c2,_,_)) ->
@@ -903,7 +905,7 @@ and eqappr cv_pb infos appr1 appr2 =
      | (FLAMV(_,vc1,_,_), FLAMV(_,vc2,_,_)) ->
 	 bool_and_convert
            (Array.length v1 = 0 & Array.length v2 = 0)
-           (forall2_conv 
+           (convert_forall2 
 	      (ccnv cv_pb infos (el_lift el1) (el_lift el2)) vc1 vc2)
 
      | _ -> (fun _ -> NotConvertible)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 46ffc42a18..88e6e70259 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -146,11 +146,19 @@ type conversion_result =
   | Convertible of universes
   | NotConvertible
 
+type conversion_test = universes -> conversion_result
+
+val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
+
+val bool_and_convert : bool -> conversion_test -> conversion_test
+val convert_and : conversion_test -> conversion_test -> conversion_test
+val convert_or : conversion_test -> conversion_test -> conversion_test
+val convert_forall2 : 
+  ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
+
 type 'a conversion_function = 
     'a unsafe_env -> constr -> constr -> conversion_result
 
-val sort_cmp : conv_pb -> sorts -> sorts -> universes -> conversion_result
-
 val fconv : conv_pb -> 'a conversion_function
 
 (* fconv has 4 instances:
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 35731c7341..923c91d03c 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -232,6 +232,6 @@ let lookup_id id env =
     | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
 
 
-type 'b assumptions = (type_judgment,'b) env
-type environment = (type_judgment,type_judgment) env
-type context = type_judgment signature
+type 'b assumptions = (typed_type,'b) env
+type environment = (typed_type,typed_type) env
+type context = typed_type signature
diff --git a/kernel/sign.mli b/kernel/sign.mli
index d2c271a7dd..151be2029c 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -77,6 +77,6 @@ type ('b,'a) search_result =
 val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
 
 
-type 'b assumptions = (type_judgment,'b) env
-type environment = (type_judgment,type_judgment) env
-type context = type_judgment signature
+type 'b assumptions = (typed_type,'b) env
+type environment = (typed_type,typed_type) env
+type context = typed_type signature
diff --git a/kernel/term.ml b/kernel/term.ml
index 7d3b9f7ff4..2f7838b2d9 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -56,8 +56,10 @@ type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
 
-type type_judgment = sorts judge
-type term_judgment = type_judgment judge
+type typed_type = sorts judge
+type typed_term = typed_type judge
+
+let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
 type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
 
@@ -1304,7 +1306,7 @@ let hcons_term (hast,hsorts,hsp,hname,hident,hstr) =
 module Htype =
   Hashcons.Make(
     struct
-      type t = type_judgment
+      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
diff --git a/kernel/term.mli b/kernel/term.mli
index c484a68d5c..cca056228b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -53,8 +53,10 @@ type constr = sorts oper term
 
 type 'a judge = { body : constr; typ : 'a }
 
-type type_judgment = sorts judge
-type term_judgment = type_judgment judge
+type typed_type = sorts judge
+type typed_term = typed_type judge
+
+val typed_app : (constr -> constr) -> typed_type -> typed_type
 
 type conv_pb = CONV | CONV_LEQ | CONV_X | CONV_X_LEQ
 
@@ -186,11 +188,11 @@ val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr
 
    where the lenght of the $j$th context is $ij$.
 *)
-val mkFix : int array -> int -> type_judgment array -> name list 
+val mkFix : int array -> int -> typed_type array -> name list 
   -> constr array -> constr
 
 (* Similarly, but we assume the body already constructed *)
-val mkFixDlam : int array -> int -> type_judgment array
+val mkFixDlam : int array -> int -> typed_type array
   -> constr array -> constr 
 
 (* If [typarray = [|t1,...tn|]]
@@ -207,11 +209,11 @@ val mkFixDlam : int array -> int -> type_judgment array
      ...
      with       fn = bn.]
  *)
-val mkCoFix : int -> type_judgment array -> name list 
+val mkCoFix : int -> typed_type array -> name list 
   -> constr array -> constr
 
 (* Similarly, but we assume the body already constructed *)
-val mkCoFixDlam : int -> type_judgment array -> constr array -> constr
+val mkCoFixDlam : int -> typed_type array -> constr array -> constr
 
 
 (*s Term destructors. 
@@ -303,10 +305,10 @@ val destCase : constr -> case_info * constr * constr * constr array
 val destGralFix : 
   constr array -> constr array * Names.name list * constr array
 val destFix : constr -> 
-  int array * int * type_judgment array * Names.name list * constr array
+  int array * int * typed_type array * Names.name list * constr array
 
 val destCoFix : 
-  constr -> int * type_judgment array * Names.name list * constr array
+  constr -> int * typed_type array * Names.name list * constr array
 
 (* Provisoire, le temps de maitriser les cast *)
 val destUntypedFix : 
@@ -524,6 +526,6 @@ val hcons_constr:
   ->
     (constr -> constr) *
     (constr -> constr) *
-    (type_judgment -> type_judgment)
+    (typed_type -> typed_type)
 
 val hcons1_constr : constr -> constr
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 392b9544f5..e20a1f0677 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -15,6 +15,8 @@ type universes
 
 val initial_universes : universes
 
+val super : universe -> universes -> universe * universes
+
 type constraint_result = 
   | Consistent of universes
   | Inconsistent