mach et himsg; typage sans extraction

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

18 files changed, 1351 insertions, 231 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index fa174d6109..f4cee1c83a 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -649,7 +649,7 @@ let inject constr = freeze ESID constr
  * just writing a "*" if it is in normal form
  *)
 let prfconstr v =
-  let pv = Printer.prterm (term_of_freeze v) in
+  let pv = Printer.pr_term (term_of_freeze v) in
   if v.norm then [< 'sTR"*"; pv >] else pv
 
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index c8e6b60060..adf7cc9ff5 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,3 +46,12 @@ let id_of_name_using_hdchar a = function
 let named_hd a = function
   | Anonymous -> Name (id_of_string (hdchar a)) 
   | x         -> x
+
+(* Judgments. *)
+
+type unsafe_judgment = { 
+  uj_val : constr;
+  uj_type : constr;
+  uj_kind : constr }
+
+
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ec148edaa6..60006e82f8 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -7,30 +7,35 @@ open Constant
 open Inductive
 open Evd
 open Univ
+open Sign
 
 type 'a unsafe_env
 
 val evar_map : 'a unsafe_env -> 'a evar_map
 val universes : 'a unsafe_env -> universes
 val metamap : 'a unsafe_env -> (int * constr) list
+val context : 'a unsafe_env -> environment
 
 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 add_mind : mutual_inductive_entry -> 'a unsafe_env -> 'a unsafe_env
 
 val new_meta : unit -> int
 
 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_mind : section_path -> 'a unsafe_env -> mutual_inductive_entry
+val lookup_mind_specif : constr -> 'a unsafe_env -> mind_specif
 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
 val named_hd : 'a unsafe_env -> constr -> name -> name
+val prod_name : name * constr * constr -> constr
 
 val translucent_abst : 'a unsafe_env -> constr -> bool
 val evaluable_abst : 'a unsafe_env -> constr -> bool
@@ -51,3 +56,9 @@ val mind_of_path : section_path -> mutual_inductive_entry
 val mind_path : constr -> section_path
 val mind_nparams : 'a unsafe_env -> constr -> int
 val mindsp_nparams : 'a unsafe_env -> section_path -> int
+
+type unsafe_judgment = { 
+  uj_val : constr;
+  uj_type : constr;
+  uj_kind : constr }
+
diff --git a/kernel/himsg.ml b/kernel/himsg.ml
new file mode 100644
index 0000000000..94ef462589
--- /dev/null
+++ b/kernel/himsg.ml
@@ -0,0 +1,161 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Printer
+open Generic
+open Term
+open Sign
+open Environ
+open Reduction
+
+let error_unbound_rel k env n =
+  let ctx = context env in
+  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
+  errorlabstrm "unbound rel"
+    [< 'sTR"Unbound reference: "; pe; 'fNL;
+       'sTR"The reference "; 'iNT n; 'sTR" is free" >]
+
+let error_cant_execute k env c =
+  let tc = gen_pr_term k env c in
+  errorlabstrm "Cannot execute"
+    [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
+
+let error_not_type k env c =
+  let ctx = context env in
+  let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
+  let pc = gen_pr_term k env c in
+  errorlabstrm "Not a type"
+    [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
+       'sTR"should be typed by Set, Prop or Type." >];;
+
+let error_assumption k env c =
+  let pc = gen_pr_term k env c in
+  errorlabstrm "Bad assumption"
+    [< 'sTR "Cannot declare a variable or hypothesis over the term";
+       'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
+
+let error_reference_variables id =
+  errorlabstrm "construct_reference" 
+    [< 'sTR "the constant"; 'sPC; pr_id id; 'sPC; 
+       'sTR "refers to variables which are not in the context" >]
+
+let error_elim_expln env kp ki=
+  if is_info_sort env kp && not (is_info_sort env ki) then
+    "non-informative objects may not construct informative ones."
+  else 
+    match (kp,ki) with 
+      | (DOP0(Sort (Type _)), DOP0(Sort (Prop _))) ->
+          "strong elimination on non-small inductive types leads to paradoxes."
+      | _ -> "wrong arity"
+
+let msg_bad_elimination env k = function
+  | Some(ki,kp,explanation) ->
+      let pki = gen_pr_term k env ki in
+      let pkp = gen_pr_term k env kp in
+      (hOV 0 
+         [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
+            pki; 'bRK(1,0);
+            'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
+            'sTR "because"; 'sPC; 'sTR explanation >])
+  | None -> [<>]
+
+let error_elim_arity k env ind aritylst c p pt okinds = 
+  let pi = gen_pr_term k env ind in
+  let ppar = prlist_with_sep pr_coma (gen_pr_term k env) aritylst in
+  let pc = gen_pr_term k env c in
+  let pp = gen_pr_term k env p in
+  let ppt = gen_pr_term k env pt in
+  errorlabstrm "incorrect elimimnation arity"
+    [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
+       'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
+       'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
+       'sTR "has type"; 'bRK(1,1); ppt; 'fNL;
+       'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
+       msg_bad_elimination env k okinds >]
+
+let error_case_not_inductive k env c ct =
+  let pc = gen_pr_term k env c in
+  let pct = gen_pr_term k env ct in
+  errorlabstrm "Cases on non inductive type"
+    [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; 
+       'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
+       'sTR "which is not an inductive definition" >]
+
+let error_number_branches k env c ct expn =
+  let pc = gen_pr_term k env c in
+  let pct = gen_pr_term k env ct in
+  errorlabstrm "Cases with wrong number of cases"
+    [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
+       'sTR "of type"; 'bRK(1,1); pct; 'sPC;
+       'sTR "expects ";  'iNT expn; 'sTR " branches" >]
+
+let error_ill_formed_branch k env c i actty expty =
+  let pc = gen_pr_term k env c in
+  let pa = gen_pr_term k env actty in
+  let pe = gen_pr_term k env expty in
+  errorlabstrm "Ill-formed branches" 
+    [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc;
+       'sPC; 'sTR "the branch " ; 'iNT (i+1);
+       'sTR " has type"; 'bRK(1,1); pa ; 'sPC; 
+       'sTR "which should be:"; 'bRK(1,1); pe >]
+
+let error_generalization k env (name,var) c =
+  let pe = pr_ne_env [< 'sTR"in environment" >] k (context env) in
+  let pv = gen_pr_term k env var.body in
+  let pc = gen_pr_term k (push_rel (name,var) env) c in
+  errorlabstrm "gen_rel"
+    [< 'sTR"Illegal generalization: "; pe; 'fNL;
+       'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
+       'sTR"over"; 'bRK(1,1); pc; 'sPC;
+       'sTR"which should be typed by Set, Prop or Type." >]
+
+let error_actual_type k env cj tj =
+  let pe = pr_ne_env [< 'sTR"In environment" >] k (context env) in
+  let pc = gen_pr_term k env cj.uj_val in
+  let pct = gen_pr_term k env cj.uj_type in
+  let pt = gen_pr_term k env tj.uj_val in
+  errorlabstrm "Bad cast"
+    [< pe; 'fNL;
+       'sTR"The term"; 'bRK(1,1); pc ; 'sPC ;
+       'sTR"does not have type"; 'bRK(1,1); pt; 'fNL;
+       'sTR"Actually, it has type" ; 'bRK(1,1); pct >]
+
+let error_cant_apply s k env rator randl =
+  let pe = pr_ne_env [< 'sTR"in environment" >] k (context env) in
+  let pr = gen_pr_term k env rator.uj_val in
+  let prt = gen_pr_term k env rator.uj_type in
+  let term_string = if List.length randl > 1 then "terms" else "term" in
+  let appl = 
+    prlist_with_sep pr_fnl
+      (fun c ->
+         let pc = gen_pr_term k env c.uj_val in
+         let pct = gen_pr_term k env c.uj_type in
+         hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl 
+  in
+  errorlabstrm "Illegal application"
+    [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; pe; 'fNL;
+       'sTR"The term"; 'bRK(1,1); pr; 'sPC;
+       'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
+       'sTR("cannot be applied to the "^term_string); 'fNL; 
+       'sTR" "; v 0 appl >]
+
+(* (co)fixpoints *)
+let error_ill_formed_rec_body str k env lna i vdefs =
+  let pvd = gen_pr_term k env vdefs.(i) in
+  errorlabstrm "Ill-formed rec body"
+    [< str; 'fNL; 'sTR"The ";
+       if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
+       'sTR"recursive definition"; 'sPC ; pvd; 'sPC;
+       'sTR "is not well-formed" >]
+    
+let error_ill_typed_rec_body k env i lna vdefj vargs =
+  let pvd = gen_pr_term k env (vdefj.(i)).uj_val in
+  let pvdt = gen_pr_term k env (vdefj.(i)).uj_type in
+  let pv = gen_pr_term k env (body_of_type vargs.(i)) in
+  errorlabstrm "Ill-typed rec body"
+    [< 'sTR"The " ;
+       if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];
+       'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
+       'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
diff --git a/kernel/himsg.mli b/kernel/himsg.mli
index f51f427604..644bfe8be9 100644
--- a/kernel/himsg.mli
+++ b/kernel/himsg.mli
@@ -12,3 +12,43 @@ open Environ
 val error_unbound_rel : path_kind -> 'a unsafe_env -> int -> 'b
 
 val error_cant_execute : path_kind -> 'a unsafe_env -> constr -> 'b
+
+val error_not_type : path_kind -> 'a unsafe_env -> constr -> 'b
+
+val error_assumption : path_kind -> 'a unsafe_env -> constr -> 'b
+ 
+val error_reference_variables : identifier -> 'a
+
+val error_elim_expln : 'a unsafe_env -> constr -> constr -> string
+
+val error_elim_arity : 
+  path_kind -> 'a unsafe_env -> constr -> constr list -> constr 
+    -> constr -> constr -> (constr * constr * string) option -> 'b
+
+val error_case_not_inductive : 
+  path_kind -> 'a unsafe_env -> constr -> constr -> 'b
+
+val error_number_branches : 
+  path_kind -> 'a unsafe_env -> constr -> constr -> int -> 'b
+
+val error_ill_formed_branch :
+  path_kind -> 'a unsafe_env -> constr -> int -> constr -> constr -> 'b
+
+val error_generalization :
+  path_kind -> 'a unsafe_env -> name * typed_type -> constr -> 'b
+
+val error_actual_type :
+  path_kind -> 'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> 'b
+
+val error_cant_apply : 
+  string -> path_kind -> 'a unsafe_env -> unsafe_judgment 
+    -> unsafe_judgment list -> 'b
+
+val error_ill_formed_rec_body :
+  std_ppcmds -> path_kind -> 'a unsafe_env 
+    -> name list -> int -> constr array -> 'b
+
+val error_ill_typed_rec_body  :
+  path_kind -> 'a unsafe_env -> int -> name list -> unsafe_judgment array 
+    -> typed_type array -> 'b
+
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 32d844e9a7..d3022c5697 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -2,11 +2,50 @@
 (* $Id$ *)
 
 open Names
+open Term
+open Sign
 
-type mind_entry
+type recarg = 
+  | Param of int 
+  | Norec 
+  | Mrec of int 
+  | Imbr of section_path * int * (recarg list)
 
-type mutual_inductive_body
+type mutual_inductive_packet = {
+  mind_consnames : identifier array;
+  mind_typename : identifier;
+  mind_lc : constr;
+  mind_stamp : name;
+  mind_arity : typed_type;
+  mind_lamexp : constr option;
+  mind_kd : sorts list;
+  mind_kn : sorts list;
+  mind_listrec : (recarg list) array;
+  mind_finite : bool }
+
+type mutual_inductive_body = {
+  mind_kind : path_kind;
+  mind_ntypes : int;
+  mind_hyps : typed_type signature;
+  mind_packets : mutual_inductive_packet array;
+  mind_singl : constr option;
+  mind_nparams : int }
 
 type mutual_inductive_entry = section_path * mutual_inductive_body
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
+
+type mind_specif = {
+  mis_sp : section_path;
+  mis_mib : mutual_inductive_body;
+  mis_tyi : int;
+  mis_args : constr array;
+  mis_mip : mutual_inductive_packet }
+
+val mis_ntypes : mind_specif -> int
+val mis_nconstr : mind_specif -> int
+val mis_nparams : mind_specif -> int
+val mis_kd : mind_specif -> sorts list
+val mis_kn : mind_specif -> sorts list
+val mis_recargs : mind_specif -> (recarg list) array array
+
diff --git a/kernel/mach.ml b/kernel/mach.ml
index 7501b45b7b..c2817f5bfd 100644
--- a/kernel/mach.ml
+++ b/kernel/mach.ml
@@ -9,10 +9,12 @@ open Generic
 open Term
 open Himsg
 open Reduction
+open Sign
 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
@@ -32,28 +34,18 @@ let tjudge_of_judge env j =
 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
- *)
+(*s The machine flags. 
+   [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$)
+   like [Acc_rec.fw].
+   [nocheck] indicates if we can skip some verifications to accelerate
+   the type inference. *)
 
 type 'a mach_flags = {
-  nofix : bool;
-  nocheck : bool;
-  noverify : bool }
+  fix : bool;
+  nocheck : bool }
+
+(* The typing machine without information. *)
 
-(* 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
@@ -83,13 +75,14 @@ let rec execute mf env cstr =
 	  error "Cannot typecheck an unevaluable abstraction"
 	      
     | IsConst _ ->
-        (make_judge cstr (type_of_const env cstr), u0)
+        (make_judge cstr (type_of_constant_or_existential env cstr), u0)
 	  
     | IsMutInd _ ->
-	(make_judge cstr (type_of_mind env cstr), u0)
+	(make_judge cstr (type_of_inductive env cstr), u0)
 	  
     | IsMutConstruct _ -> 
-        (make_judge cstr (type_of_mconstr env cstr), u0)
+	let (typ,kind) = destCast (type_of_constructor env cstr) in
+        ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , u0)
 	  
     | IsMutCase (_,p,c,lf) ->
         let (cj,u1) = execute mf env c in
@@ -101,7 +94,7 @@ let rec execute mf env cstr =
         (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
+        if (not mf.fix) && 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
@@ -115,7 +108,7 @@ let rec execute mf env cstr =
 	(make_judge cofix larv.(i), u1)
 	  
     | IsSort (Prop c) -> 
-	(type_of_proposition c, u0)
+	(type_of_prop_or_set c, u0)
 
     | IsSort (Type u) ->
 	type_of_type u u0
@@ -137,7 +130,7 @@ let rec execute mf env cstr =
 	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)
+        abs_rel env2 name var j'
 	  
     | IsProd (name,c1,c2) ->
         let (j,u1) = execute mf env c1 in
@@ -145,7 +138,7 @@ let rec execute mf env cstr =
 	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)
+        gen_rel env2 name var j'
 	  
     | IsCast (c,t) ->
         let (cj,u1) = execute mf env c in
@@ -182,186 +175,64 @@ and execute_list mf env = function
       (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))
+(* The typed type of a judgment. *)
 
-*)
-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 execute_type mf env constr = 
+  let (j,_) = execute mf env constr in
+  typed_type_of_judgment env j
+
+
+(* Exported machines.  First safe machines, with no general fixpoint
+   allowed (the flag [fix] is not set) and all verifications done (the
+   flag [nocheck] is not set). *)
+
+let safe_machine env constr = 
+  let mf = { fix = false; nocheck = false } in
+  execute mf env constr
+
+let safe_machine_type env constr = 
+  let mf = { fix = false; nocheck = false } in
+  execute_type mf env constr
+
+(* Machines with general fixpoint. *)
+
+let fix_machine env constr = 
+  let mf = { fix = true; nocheck = false } in
+  execute mf env constr
+
+let fix_machine_type env constr = 
+  let mf = { fix = true; nocheck = false } in
+  execute_type mf env constr
+
+(* Fast machines without any verification. *)
+
+let unsafe_machine env constr = 
+  let mf = { fix = true; nocheck = true } in
+  execute mf env constr
+
+let unsafe_machine_type env constr = 
+  let mf = { fix = true; nocheck = true } in
+  execute_type mf env constr
+
+
+(* ``Type of'' machines. *)
 
+let type_of env c = 
+  let (j,_) = safe_machine env c in nf_betaiota env j.uj_type
 
-let castify_sign sigma sign = sign_of_sign sigma sign
+let type_of_type env c = 
+  let tt = safe_machine_type env c in DOP0 (Sort tt.typ)
 
-let castify_env sigma env =
-  let sign = (* castify_sign sigma *) (get_globals env)
-  in env_of_env sigma (ENVIRON(sign,get_rels env))
+let unsafe_type_of env c = 
+  let (j,_) = unsafe_machine env c in nf_betaiota env j.uj_type
 
+let unsafe_type_of_type env c = 
+  let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
 
-(* Fin fonctions pour l'inversion *)
 
-(**)
+(*s Machines with information. *)
 
+(*i
 let implicit_judgment = {body=mkImplicit;typ=implicit_sort}
 
 let add_inf_rel (na,inf) env =
@@ -724,3 +595,4 @@ let infexecute_type_with_univ sigma psign sp c =
 
 let infexecute_with_univ sigma psign sp c =
   with_universes (infexecute sigma psign) (sp,initial_universes,c) 
+i*)
diff --git a/kernel/mach.mli b/kernel/mach.mli
index 701c2a58f8..fbf1a3ef7a 100644
--- a/kernel/mach.mli
+++ b/kernel/mach.mli
@@ -10,30 +10,27 @@ open Environ
 open Machops
 (*i*)
 
-(*s Machine without information. *)
+(*s Machines without information. *)
 
-val fexecute_type : 'a unsafe_env -> constr -> typed_type
-val fexecute : 'a unsafe_env -> constr -> unsafe_judgment
+val safe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
+val safe_machine_type : 'a unsafe_env -> constr -> typed_type
 
-val execute_rec_type : 'a unsafe_env -> constr -> typed_type
-val execute_rec : 'a unsafe_env -> constr -> unsafe_judgment
+val fix_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
+val fix_machine_type : 'a unsafe_env -> constr -> typed_type
+
+val unsafe_machine : 'a unsafe_env -> constr -> unsafe_judgment * universes
+val unsafe_machine_type : 'a unsafe_env -> constr -> typed_type
 
 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 type_of_type : '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. *)
 
+(*i
 val infexemeta : 
   'a unsafe_env -> constr -> unsafe_judgment * information * universes
 
@@ -46,3 +43,4 @@ val infexecute :
 val inf_env_of_env : 'a unsafe_env -> 'a unsafe_env
 
 val core_infmachine : 'a unsafe_env -> constr -> information
+i*)
diff --git a/kernel/machops.ml b/kernel/machops.ml
new file mode 100644
index 0000000000..8d79cac17f
--- /dev/null
+++ b/kernel/machops.ml
@@ -0,0 +1,924 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Univ
+open Generic
+open Term
+open Evd
+open Constant
+open Inductive
+open Sign
+open Environ
+open Reduction
+open Himsg
+
+type information = Logic | Inf of unsafe_judgment
+
+let make_judge v tj =
+  { uj_val = v;
+    uj_type = tj.body;
+    uj_kind= DOP0 (Sort tj.typ) }
+
+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 j =
+  match whd_betadeltaiota env j.uj_type with
+    | DOP0(Sort s) -> { body = j.uj_val; typ = s }
+    | _ -> error_not_type CCI env j.uj_val
+
+let assumption_of_judgement env j =
+  match whd_betadeltaiota env j.uj_type with
+    | DOP0(Sort s) -> { body = j.uj_val; typ = 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 typ.body;
+      uj_kind = DOP0 (Sort typ.typ) }
+  with Not_found -> 
+    error_unbound_rel CCI env n
+
+(* Management of context of variables. *)
+
+(* Checks if a context of variable is included in another one. *)
+
+let hyps_inclusion env (idl1,tyl1) (idl2,tyl2) =
+  let rec aux = function
+    | ([], [], _, _) -> true
+    | (_, _, [], []) -> false
+    | ((id1::idl1), (ty1::tyl1), idl2, tyl2) ->
+        let rec search = function
+          | ([], []) -> false
+          | ((id2::idl2), (ty2::tyl2)) ->
+              if id1 = id2 then
+		(is_conv env (body_of_type ty1) (body_of_type ty2))
+		& aux (idl1,tyl1,idl2,tyl2)
+              else 
+		search (idl2,tyl2)
+          | (_, _) -> invalid_arg "hyps_inclusion"
+        in 
+	search (idl2,tyl2)
+    | (_, _, _, _) -> invalid_arg "hyps_inclusion"
+  in
+  aux (idl1,tyl1,idl2,tyl2) 
+
+(* Checks if the given context of variables [hyps] is included in the
+   current context of [env]. *)
+
+let construct_reference id env hyps =
+  let hyps' = get_globals (context env) in
+  if hyps_inclusion env hyps hyps' then
+    Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))
+  else 
+    error_reference_variables id
+
+let check_hyps id env hyps =
+  let hyps' = get_globals (context env) in
+  if not (hyps_inclusion env hyps hyps') then
+    error_reference_variables id
+
+(* Instantiation of terms on real arguments. *)
+
+let is_id_inst ids args =
+  let is_id id = function
+    | VAR id' -> id = id'
+    | _ -> false
+  in
+  List.for_all2 is_id ids args
+
+let instantiate_constr ids c args =
+  if is_id_inst ids args then
+    c
+  else
+    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 }
+
+(* Constants. *)
+
+let constant_reference env sp =
+  let (_,cb) = lookup_constant sp env in
+  (Const sp, construct_reference (basename sp) env cb.const_hyps)
+
+let type_of_constant env c =
+  let (sp,args) = destConst c in
+  let (_,cb) = lookup_constant sp env in
+  let hyps = cb.const_hyps in
+  check_hyps (basename sp) env hyps;
+  instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
+
+(* Existentials. *)
+
+let type_of_existential env c =
+  let (sp,args) = destConst c in
+  let info = Evd.map (evar_map env) sp in
+  let hyps = info.evar_hyps in
+  check_hyps (basename sp) env hyps;
+  instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+
+(* Constants or existentials. *)
+
+let type_of_constant_or_existential env c =
+  if is_existential c then
+    type_of_existential env c
+  else
+    type_of_constant env c
+
+(* Inductive types. *)
+
+let instantiate_arity mis =
+  let ids = ids_of_sign mis.mis_mib.mind_hyps in
+  let args = Array.to_list mis.mis_args in 
+  let arity = mis.mis_mip.mind_arity in
+  { body = instantiate_constr ids arity.body args;
+    typ = arity.typ }
+
+let type_of_inductive env i =
+  let mis = lookup_mind_specif i env in
+  let hyps = mis.mis_mib.mind_hyps in
+  check_hyps (basename mis.mis_sp) env hyps;
+  instantiate_arity mis
+
+(* Constructors. *)
+
+let instantiate_lc mis =
+  let hyps = mis.mis_mib.mind_hyps in
+  let lc = mis.mis_mip.mind_lc in
+  instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args)
+
+let type_of_constructor env c =
+  let (sp,i,j,args) = destMutConstruct c in
+  let mind = DOPN (MutInd (sp,i), args) in
+  let recmind = check_mrectype_spec env mind in
+  let mis = lookup_mind_specif recmind env in
+  check_hyps (basename mis.mis_sp) env (mis.mis_mib.mind_hyps);
+  let specif = instantiate_lc mis in
+  let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in
+  if j > mis_nconstr mis then
+    anomaly "type_of_constructor"
+  else
+    sAPPViList (j-1) specif (list_tabulate make_ik (mis_ntypes mis))
+
+(* gives the vector of constructors and of 
+   types of constructors of an inductive definition 
+   correctly instanciated *)
+
+let mis_type_mconstructs mis =
+  let specif = instantiate_lc mis
+  and ntypes = mis_ntypes mis
+  and nconstr = mis_nconstr mis in
+  let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) 
+  and make_ck k = 
+    DOPN (MutConstruct ((mis.mis_sp,mis.mis_tyi),k+1), mis.mis_args) 
+  in
+  (Array.init nconstr make_ck, 
+   sAPPVList specif (list_tabulate make_ik ntypes))
+
+let type_mconstructs env mind =
+  let redmind  = check_mrectype_spec env mind in
+  let mis = lookup_mind_specif redmind env in 
+  mis_type_mconstructs mis
+
+(* Case. *)
+
+let rec sort_of_arity env c =
+  match whd_betadeltaiota env c with
+    | DOP0(Sort( _)) as c' -> c'
+    | DOP2(Prod,_,DLAM(_,c2)) -> sort_of_arity env c2
+    | _ -> invalid_arg "sort_of_arity"
+
+let make_arity_dep env k = 
+  let rec mrec c m = match whd_betadeltaiota env c with 
+    | DOP0(Sort _) -> mkArrow m k
+    | DOP2(Prod,b,DLAM(n,c_0)) ->
+        prod_name (n,b,mrec c_0 (applist(lift 1 m,[Rel 1])))
+    | _ -> invalid_arg "make_arity_dep"
+  in 
+  mrec
+
+let make_arity_nodep env k = 
+  let rec mrec c = match whd_betadeltaiota env c with 
+    | DOP0(Sort _) -> k
+    | DOP2(Prod,b,DLAM(x,c_0)) -> DOP2(Prod,b,DLAM(x,mrec c_0))
+    | _ -> invalid_arg "make_arity_nodep"
+  in 
+  mrec
+
+exception Arity of (constr * constr * string) option
+
+let is_correct_arity env kd kn (c,p) = 
+  let rec srec ind (pt,t) =
+    try 
+      (match whd_betadeltaiota env pt, whd_betadeltaiota env t with
+	 | DOP2(Prod,a1,DLAM(_,a2)), DOP2(Prod,a1',DLAM(_,a2')) ->
+             if is_conv env a1 a1' then
+               srec (applist(lift 1 ind,[Rel 1])) (a2,a2') 
+             else 
+	       raise (Arity None)
+	 | DOP2(Prod,a1,DLAM(_,a2)), ki -> 
+             let k = whd_betadeltaiota env a2 in 
+             let ksort = (match k with DOP0(Sort s) -> s 
+			    | _ -> raise (Arity None)) in
+             if is_conv env a1 ind then
+               if List.exists (base_sort_cmp CONV ksort) kd then
+		 (true,k)
+               else 
+		 raise (Arity (Some(k,ki,error_elim_expln env k ki)))
+	     else 
+	       raise (Arity None)
+	 | k, DOP2(Prod,_,_) ->
+	     raise (Arity None)
+	 | k, ki -> 
+	     let ksort = (match k with DOP0(Sort s) -> s 
+                            | _ ->  raise (Arity None)) in
+             if List.exists (base_sort_cmp CONV ksort) kn then 
+	       false,k
+             else 
+	       raise (Arity (Some(k,ki,error_elim_expln env k ki))))
+    with Arity kinds ->
+      let listarity =
+	(List.map (fun s -> make_arity_dep env (DOP0(Sort s)) t ind) kd)
+	@(List.map (fun s -> make_arity_nodep env (DOP0(Sort s)) t) kn)
+      in error_elim_arity CCI env ind listarity c p pt kinds
+  in srec 
+
+let cast_instantiate_arity mis =
+  let tty = instantiate_arity mis in
+  DOP2 (Cast, tty.body, DOP0 (Sort tty.typ))
+
+let find_case_dep_nparams env (c,p) (mind,largs) typP =    
+  let mis = lookup_mind_specif mind env in 
+  let nparams = mis_nparams mis
+  and kd = mis_kd mis 
+  and kn = mis_kn mis
+  and t = cast_instantiate_arity mis in 
+  let (globargs,la) = list_chop nparams largs in
+  let glob_t = hnf_prod_applist env "find_elim_boolean" t globargs in
+  let arity = applist(mind,globargs) in
+  let (dep,_) = is_correct_arity env kd kn (c,p) arity (typP,glob_t) in
+  (dep, (nparams, globargs,la))
+
+let type_one_branch_dep (env,nparams,globargs,p) co t = 
+  let rec typrec n c =
+    match whd_betadeltaiota env c with
+      | DOP2(Prod,a1,DLAM(x,a2)) -> prod_name (x,a1,typrec (n+1) a2)
+      | x -> let lAV = destAppL (ensure_appl x) in
+             let (_,vargs) = array_chop (nparams+1) lAV in
+             applist 
+               (appvect ((lift n p),vargs),
+		[applist(co,((List.map (lift n) globargs)@(rel_list 0 n)))])
+  in 
+  typrec 0 (hnf_prod_applist env "type_case" t globargs)
+
+let type_one_branch_nodep (env,nparams,globargs,p) t = 
+  let rec typrec n c =
+    match whd_betadeltaiota env c with 
+      | DOP2(Prod,a1,DLAM(x,a2)) -> DOP2(Prod,a1,DLAM(x,typrec (n+1) a2))
+      | x -> let lAV = destAppL(ensure_appl x) in
+             let (_,vargs) = array_chop (nparams+1) lAV in
+             appvect (lift n p,vargs)
+  in 
+  typrec 0 (hnf_prod_applist env "type_case" t globargs)
+
+(* type_case_branches type un <p>Case c of ... end 
+   ct = type de c, si inductif il a la forme APP(mI,largs), sinon raise Induc
+   pt = sorte de p
+   type_case_branches retourne (lb, lr); lb est le vecteur des types
+   attendus dans les branches du Case; lr est le type attendu du resultat
+ *)
+
+let type_case_branches env ct pt p c =
+  try
+    let ((mI,largs) as indt) = find_mrectype env ct in
+    let (dep,(nparams,globargs,la)) =
+      find_case_dep_nparams env (c,p) indt pt
+    in
+    let (lconstruct,ltypconstr) = type_mconstructs env mI in
+    if dep then 
+      (mI, 
+       array_map2 (type_one_branch_dep (env,nparams,globargs,p))
+         lconstruct ltypconstr,
+         beta_applist (p,(la@[c])))
+    else 
+      (mI,
+       Array.map (type_one_branch_nodep (env,nparams,globargs,p)) 
+         ltypconstr,
+         beta_applist (p,la))
+  with Induc -> 
+    error_case_not_inductive CCI env c ct
+
+let check_branches_message env (c,ct) (explft,lft) = 
+  let n = Array.length explft 
+  and expn = Array.length lft in
+  let rec check_conv i = 
+    if not (i = n) then
+      if not (is_conv_leq env lft.(i) (explft.(i))) then
+	error_ill_formed_branch CCI env c i (nf_betaiota env lft.(i))
+	  (nf_betaiota env explft.(i))
+      else 
+	check_conv (i+1) 
+  in
+  if n<>expn then error_number_branches CCI env c ct expn else check_conv 0
+
+let type_of_case env pj cj lfj =
+  let lft = Array.map (fun j -> j.uj_type) lfj in
+  let (mind,bty,rslty) =
+    type_case_branches env cj.uj_type pj.uj_type pj.uj_val cj.uj_val in
+  let kind = sort_of_arity env pj.uj_type in
+  check_branches_message env (cj.uj_val,cj.uj_type) (bty,lft);
+  { uj_val  = 
+      mkMutCaseA (ci_of_mind mind) (j_val pj) (j_val cj) (Array.map j_val lfj);
+    uj_type = rslty;
+    uj_kind = kind }
+
+(* Prop and Set *)
+
+let type_of_prop_or_set cts =
+  { uj_val = DOP0(Sort(Prop cts));
+    uj_type = DOP0(Sort type_0);
+    uj_kind = DOP0(Sort type_1) }
+
+(* Type of Type(i). *)
+
+let type_of_type u g =
+  let (uu,g') = super u g in
+  let (uuu,g'') = super uu g' in
+  { uj_val = DOP0 (Sort (Type u));
+    uj_type = DOP0 (Sort (Type uu));
+    uj_kind = DOP0 (Sort (Type uuu)) },
+  g''
+
+let type_of_sort c g =
+  match c with
+    | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g'
+    | DOP0 (Sort (Prop _)) -> mkType prop_univ, g
+    | DOP0 (Implicit) -> mkImplicit, g
+    | _ -> invalid_arg "type_of_sort"
+
+(* Type of a lambda-abstraction. *)
+
+let sort_of_product domsort rangsort g0 =
+  match rangsort with
+    (* Product rule (s,Prop,Prop) *) 
+    | Prop _ -> rangsort, g0
+    | Type u2 ->
+        (match domsort with
+           (* Product rule (Prop,Type_i,Type_i) *)
+           | Prop _ -> rangsort, g0
+           (* Product rule (Type_i,Type_i,Type_i) *) 
+           | Type u1 -> let (u12,g1) = sup u1 u2 g0 in Type u12, g1)
+
+let abs_rel env name var j =
+  let rngtyp = whd_betadeltaiota env j.uj_kind in
+  let cvar = incast_type var in
+  let (s,g) = sort_of_product var.typ (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 },
+  g
+
+(* Type of a product. *)
+
+let gen_rel env name var j =
+  let jtyp = whd_betadeltaiota env j.uj_type in
+  let jkind = whd_betadeltaiota env 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 var.typ s (universes env) in
+          let res_type = mkSort s' in
+	  let (res_kind,g') = type_of_sort res_type g in
+          { uj_val = 
+	      mkProd name (mkCast var.body (mkSort var.typ)) (j_val_cast j);
+            uj_type = res_type;
+            uj_kind = res_kind }, g'
+      | _ -> 
+	  error_generalization CCI env (name,var) j.uj_val
+
+(* Type of a cast. *)
+	    
+let cast_rel env cj tj =
+  if is_conv_leq env cj.uj_type tj.uj_val then
+    { uj_val = j_val_only cj;
+      uj_type = tj.uj_val;
+      uj_kind = whd_betadeltaiota env tj.uj_type }
+  else 
+    error_actual_type CCI env cj tj
+
+(* Type of an application. *)
+
+let apply_rel_list env0 nocheck argjl funj =
+  let rec apply_rec env typ = function
+    | [] -> 
+	{ uj_val  = applist (j_val_only funj, List.map j_val_only argjl);
+          uj_type = typ;
+          uj_kind = funj.uj_kind },
+	universes env
+    | hj::restjl ->
+        match whd_betadeltaiota env typ with
+          | DOP2(Prod,c1,DLAM(_,c2)) ->
+              if nocheck then
+                apply_rec env (subst1 hj.uj_val c2) restjl
+	      else 
+		(match conv_leq env hj.uj_type c1 with
+		   | Convertible g ->
+		       let env' = set_universes g env in
+		       apply_rec env' (subst1 hj.uj_val c2) restjl
+		   | NotConvertible -> 
+		       error_cant_apply "Type Error" CCI env funj argjl)
+          | _ ->
+              error_cant_apply "Non-functional construction" CCI env funj argjl
+  in 
+  apply_rec env0 funj.uj_type argjl
+
+
+(* Fixpoints. *)
+
+(* Checking function for terms containing existential variables.
+ The function noccur_with_meta consideres the fact that
+ each existential variable (as well as each isevar)
+ in the term appears applied to its local context,
+ which may contain the CoFix variables. These occurrences of CoFix variables
+ are not considered *)
+
+let noccur_with_meta sigma n m term = 
+  let rec occur_rec n = function
+    | Rel(p) -> if n<=p & p<n+m then raise Occur
+    | VAR _ -> ()
+    | DOPN(AppL,cl) ->
+	(match strip_outer_cast cl.(0) with
+           | DOP0 (Meta _) -> ()
+	   | _ -> Array.iter (occur_rec n) cl)
+    | DOPN(Const sp, cl) when Evd.in_dom sigma sp -> ()
+    | DOPN(op,cl) -> Array.iter (occur_rec n) cl
+    | DOPL(_,cl) -> List.iter (occur_rec n) cl
+    | DOP0(_) -> ()
+    | DOP1(_,c) -> occur_rec n c
+    | DOP2(_,c1,c2) -> occur_rec n c1; occur_rec n c2
+    | DLAM(_,c) -> occur_rec (n+1) c
+    | DLAMV(_,v) -> Array.iter (occur_rec (n+1)) v
+  in 
+  try (occur_rec n term; true) with Occur -> false
+
+(* Check if t is a subterm of Rel n, and gives its specification, 
+   assuming lst already gives index of
+   subterms with corresponding specifications of recursive arguments *)
+
+(* A powerful notion of subterm *)
+
+let find_sorted_assoc p = 
+  let rec findrec = function 
+    | (a,ta)::l -> 
+	if a < p then findrec l else if a = p then ta else raise Not_found
+    | _ -> raise Not_found
+  in 
+  findrec
+
+let map_lift_fst_n m = List.map (function (n,t)->(n+m,t))
+let map_lift_fst = map_lift_fst_n 1
+
+let rec instantiate_recarg sp lrc ra = 
+  match ra with 
+    | Mrec(j)        -> Imbr(sp,j,lrc)
+    | Imbr(sp1,k,l)  -> Imbr(sp1,k, List.map (instantiate_recarg sp lrc) l)
+    | Norec          -> Norec
+    | Param(k)       -> List.nth lrc k
+
+(* propagate checking for F,incorporating recursive arguments *)
+let check_term env mind_recvec f = 
+  let rec crec n l (lrec,c) = 
+    match (lrec,strip_outer_cast c) with
+      | (Param(_)::lr,DOP2(Lambda,_,DLAM(_,b))) -> 
+          let l' = map_lift_fst l in
+          crec (n+1) l' (lr,b)
+      | (Norec::lr,DOP2(Lambda,_,DLAM(_,b))) -> 
+          let l' = map_lift_fst l in
+          crec (n+1) l' (lr,b)
+      | (Mrec(i)::lr,DOP2(Lambda,_,DLAM(_,b)))  -> 
+          let l' = map_lift_fst l in
+          crec (n+1) ((1,mind_recvec.(i))::l') (lr,b)
+      | (Imbr(sp,i,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> 
+          let l' = map_lift_fst l in
+          let sprecargs = 
+	    mis_recargs (lookup_mind_specif (mkMutInd sp i [||]) env) in
+          let lc = 
+	    Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
+	  in
+          crec (n+1) ((1,lc)::l') (lr,b)
+      | _,f_0 -> f n l f_0
+  in 
+  crec
+
+let is_inst_var env k c = 
+  match whd_betadeltaiota_stack env c [] with 
+    | (Rel n,_) -> n=k
+    | _ -> false
+
+let is_subterm_specif env lcx mind_recvec = 
+  let rec crec n lst c = 
+    match whd_betadeltaiota_stack env c [] with 
+      | ((Rel k),_) -> find_sorted_assoc k lst
+      |  (DOPN(MutCase _,_) as x,_) ->
+           let ( _,_,c,br) = destCase x in
+           if Array.length br = 0 then
+             [||] 
+           else
+             let lcv = 
+	       (try 
+		  if is_inst_var env n c then lcx else (crec n lst c) 
+                with Not_found -> (Array.create (Array.length br) []))
+             in 
+	     assert (Array.length br = Array.length lcv);
+             let stl = 
+	       array_map2
+                 (fun lc a -> 
+                    check_term env mind_recvec crec n lst (lc,a)) lcv br 
+             in 
+	     stl.(0)
+	       
+      | (DOPN(Fix(_),la) as mc,l) ->
+          let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in
+          let nbfix   = List.length funnames in
+          let decrArg = recindxs.(i) in 
+          let theBody = bodies.(i)   in
+          let (gamma,strippedBody) = decompose_lam_n (decrArg+1) theBody in
+          let absTypes = List.map snd gamma in 
+          let nbOfAbst = nbfix+decrArg+1 in
+          let newlst = 
+            if List.length l < (decrArg+1) then
+              ((nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst))
+            else 
+              let theDecrArg  = List.nth l decrArg in
+              let recArgsDecrArg = 
+                try (crec n lst theDecrArg)
+	        with Not_found -> Array.create 0 [] 
+              in 
+	      if (Array.length recArgsDecrArg)=0 then
+		(nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst)
+              else 
+		(1,recArgsDecrArg) ::
+                (nbOfAbst,lcx) ::
+                (map_lift_fst_n nbOfAbst lst)
+          in 
+	  crec (n+nbOfAbst) newlst strippedBody
+	    
+      |  (DOP2(Lambda,_,DLAM(_,b)),[]) -> 
+           let lst' = map_lift_fst lst in
+           crec (n+1) lst' b
+
+      (*** Experimental change *************************)
+      | (DOP0(Meta _),_) -> [||]
+      | _ -> raise Not_found
+  in 
+  crec
+
+let is_subterm env lcx mind_recvec n lst c = 
+  try 
+    let _ = is_subterm_specif env lcx mind_recvec n lst c in true 
+  with Not_found -> 
+    false
+
+(* Auxiliary function: it checks a condition f depending on a deBrujin
+ index  for a certain number of abstractions *)
+
+let rec check_subterm_rec_meta env vectn k def = 
+  (k < 0) or
+  (let nfi = Array.length vectn in 
+   (* check fi does not appear in the k+1 first abstractions, 
+      gives the type of the k+1-eme abstraction  *)
+   let rec check_occur n def = 
+     (match strip_outer_cast def with
+	| DOP2(Lambda,a,DLAM(_,b)) -> 
+	    if noccur_with_meta (evar_map env) n nfi a then
+              if n = k+1 then (a,b) else check_occur (n+1) b
+            else 
+	      error "Bad occurrence of recursive call"
+        | _ -> error "Not enough abstractions in the definition") in
+   let (c,d) = check_occur 1 def in 
+   let (mI, largs) = 
+     (try find_minductype env c 
+      with Induc -> error "Recursive definition on a non inductive type") in
+   let (sp,tyi,_) = destMutInd mI in
+   let mind_recvec = mis_recargs (lookup_mind_specif mI env) in 
+   let lcx = mind_recvec.(tyi)  in
+   (* n   = decreasing argument in the definition;
+      lst = a mapping var |-> recargs
+      t   = the term to be checked
+   *)
+   let rec check_rec_call n lst t = 
+     (* n gives the index of the recursive variable *)
+     (noccur_with_meta (evar_map env) (n+k+1) nfi t) or 
+     (* no recursive call in the term *)
+     (match whd_betadeltaiota_stack env t [] with 
+	| (Rel p,l) -> 
+	    if n+k+1 <= p & p < n+k+nfi+1 then
+	      (* recursive call *) 
+	      let glob = nfi+n+k-p in  (* the index of the recursive call *) 
+	      let np = vectn.(glob) in (* the decreasing arg of the rec call *)
+	      if List.length l > np then 
+		(match list_chop np l with
+		     (la,(z::lrest)) -> 
+	               if (is_subterm env lcx mind_recvec n lst z) 
+                       then List.for_all (check_rec_call n lst) (la@lrest)
+                       else error "Recursive call applied to an illegal term"
+		   | _ -> assert false)
+	      else error  "Not enough arguments for the recursive call"
+	    else List.for_all (check_rec_call n lst) l        
+	| (DOPN(MutCase _,_) as mc,l) ->
+            let (ci,p,c_0,lrest) = destCase mc in
+            let lc = 
+	      (try 
+		 if is_inst_var env n c_0 then 
+		   lcx 
+		 else 
+		   is_subterm_specif env lcx mind_recvec n lst c_0
+	       with Not_found -> 
+		 Array.create (Array.length lrest) []) 
+	    in
+            (array_for_all2
+	       (fun c_0 a -> 
+		  check_term env mind_recvec (check_rec_call) n lst (c_0,a))
+	       lc lrest) 
+	    && (List.for_all (check_rec_call n lst) (c_0::p::l)) 
+
+  (* Enables to traverse Fixpoint definitions in a more intelligent
+     way, ie, the rule :
+
+     if - g = Fix g/1 := [y1:T1]...[yp:Tp]e &
+        - f is guarded with respect to the set of pattern variables S 
+          in a1 ... am        &
+        - f is guarded with respect to the set of pattern variables S 
+          in T1 ... Tp        &
+        - ap is a sub-term of the formal argument of f &
+        - f is guarded with respect to the set of pattern variables S+{yp}
+          in e
+     then f is guarded with respect to S in (g a1 ... am).
+
+     Eduardo 7/9/98 *)
+
+	| (DOPN(Fix(_),la) as mc,l) ->
+            (List.for_all (check_rec_call n lst) l) &&
+            let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in
+            let nbfix = List.length funnames in
+            let decrArg = recindxs.(i) in
+            if (List.length l < (decrArg+1)) then
+              (array_for_all (check_rec_call n lst) la)
+            else 
+              let theDecrArg  = List.nth l decrArg in
+              let recArgsDecrArg = 
+                try (is_subterm_specif env lcx mind_recvec n lst theDecrArg)
+	        with Not_found -> Array.create 0 [] 
+              in 
+	      if (Array.length recArgsDecrArg)=0 then
+		array_for_all (check_rec_call n lst) la
+              else 
+                let theBody = bodies.(i)   in
+                let (gamma,strippedBody) = 
+		  decompose_lam_n (decrArg+1) theBody in
+                let absTypes = List.map snd gamma in 
+                let nbOfAbst = nbfix+decrArg+1 in
+                let newlst = 
+		  ((1,recArgsDecrArg)::(map_lift_fst_n nbOfAbst lst))
+                in 
+		((array_for_all
+		    (fun t -> check_rec_call n lst t)
+		    typarray) &&
+                 (list_for_all_i (fun n -> check_rec_call n lst) n absTypes) &
+                 (check_rec_call (n+nbOfAbst) newlst strippedBody))
+		
+		
+	| (DOP2(_,a,b),l) -> 
+	    (check_rec_call n lst a) &&
+            (check_rec_call n lst b) &&
+            (List.for_all (check_rec_call n lst) l)
+
+	 | (DOPN(_,la),l) -> 
+	     (array_for_all (check_rec_call n lst) la) &&
+             (List.for_all (check_rec_call n lst) l)
+
+	 | (DOP0 (Meta _),l) -> true
+
+	 | (DLAM(_,t),l) -> 
+	     (check_rec_call (n+1) (map_lift_fst lst) t) &&
+             (List.for_all (check_rec_call n lst) l)
+
+	 | (DLAMV(_,vt),l) -> 
+	     (array_for_all (check_rec_call (n+1) (map_lift_fst lst)) vt) &&
+             (List.for_all (check_rec_call n lst) l)
+
+	 | (_,l) ->  List.for_all (check_rec_call n lst) l
+     ) 
+     
+   in 
+   check_rec_call 1 [] d)
+
+(* vargs is supposed to be built from A1;..Ak;[f1]..[fk][|d1;..;dk|]
+and vdeft is [|t1;..;tk|] such that f1:A1,..,fk:Ak |- di:ti
+nvect is [|n1;..;nk|] which gives for each recursive definition 
+the inductive-decreasing index 
+the function checks the convertibility of ti with Ai *)
+
+let check_fix env = function
+  | DOPN(Fix(nvect,j),vargs) -> 
+      let nbfix = let nv = Array.length vargs in 
+      if nv < 2 then error "Ill-formed recursive definition" else nv-1 in
+      let varit = Array.sub vargs 0 nbfix in
+      let ldef = array_last vargs in
+      let ln = Array.length nvect 
+      and la = Array.length varit in
+      if ln <> la then 
+	error "Ill-formed fix term"
+      else 
+	let (lna,vdefs) = decomp_DLAMV_name ln ldef in 
+	let vlna = Array.of_list lna in
+	let check_type i = 
+	  try
+	    let _ = check_subterm_rec_meta env nvect nvect.(i) vdefs.(i) in ()
+	  with UserError (s,str) ->
+	    error_ill_formed_rec_body str CCI env lna i vdefs 
+	in
+	for i = 0 to ln-1 do check_type i done 
+
+  | _ -> assert false
+
+(* Co-fixpoints. *)
+
+let check_guard_rec_meta env nbfix def deftype = 
+  let rec codomain_is_coind c  =
+    match whd_betadeltaiota env (strip_outer_cast c) with
+      | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b 
+      | b  -> 
+	  (try find_mcoinductype env b
+           with 
+	     | Induc -> error "The codomain is not a coinductive type"
+	     | _ -> error "Type of Cofix function not as expected")
+  in
+  let (mI, _) = codomain_is_coind deftype in
+  let (sp,tyi,_) = destMutInd mI in
+  let lvlra = (mis_recargs (lookup_mind_specif mI env)) in
+  let vlra = lvlra.(tyi) in  
+  let evd = evar_map env in
+  let rec check_rec_call alreadygrd n vlra  t = 
+    if (noccur_with_meta evd n nbfix t) then
+      true 
+    else 
+      match whd_betadeltaiota_stack env t [] with 
+	| (DOP0 (Meta _), l) -> true
+	      
+	|  (Rel p,l) -> 
+             if n <= p && p < n+nbfix then
+	       (* recursive call *)
+               if alreadygrd then
+		 if List.for_all (noccur_with_meta evd n nbfix) l then
+		   true
+		 else 
+		   error "Nested recursive occurrences"
+               else 
+		 error "Unguarded recursive call"
+             else  
+	       error "check_guard_rec_meta: ???"
+		 
+	| (DOPN ((MutConstruct((x,y),i)),l), args)  ->
+            let lra =vlra.(i-1) in 
+            let mI = DOPN(MutInd(x,y),l) in
+            let _,realargs = list_chop (mind_nparams env mI) args in
+            let rec process_args_of_constr l lra =
+              match l with
+                | [] -> true 
+                | t::lr ->
+		    (match lra  with 
+                       | [] -> 
+			   anomalylabstrm "check_guard_rec_meta"
+			     [< 'sTR "a constructor with an empty list";
+				'sTR "of recargs is being applied" >]
+                       |  (Mrec i)::lrar -> 
+                            let newvlra = lvlra.(i) in
+                            (check_rec_call true n newvlra t) &&
+                            (process_args_of_constr lr lrar)
+			    
+                       |  (Imbr(sp,i,lrc)::lrar)  ->
+			    let mis =
+			      lookup_mind_specif (mkMutInd sp i [||]) env in
+                            let sprecargs = mis_recargs mis in
+                            let lc = (Array.map 
+                                        (List.map 
+                                           (instantiate_recarg sp lrc))
+                                        sprecargs.(i))
+                            in (check_rec_call true n lc t) &
+                               (process_args_of_constr lr lrar)
+				 
+                       |  _::lrar  -> 
+                            if (noccur_with_meta evd n nbfix t) 
+                            then (process_args_of_constr lr lrar)
+                            else error "Recursive call inside a non-recursive argument of constructor")
+            in (process_args_of_constr realargs lra)
+		 
+		 
+	| (DOP2(Lambda,a,DLAM(_,b)),[]) -> 
+            if (noccur_with_meta evd n nbfix a) then
+              check_rec_call alreadygrd (n+1)  vlra b
+            else 
+	      error "Recursive call in the type of an abstraction"
+	      
+	| (DOPN(CoFix(j),vargs),l) -> 
+            let nbfix = let nv = Array.length vargs in 
+            if nv < 2 then
+              error "Ill-formed recursive definition" 
+            else 
+	      nv-1 
+	    in
+            let varit = Array.sub vargs 0 nbfix in
+            let ldef = array_last vargs in
+            let la = Array.length varit in
+            let (lna,vdefs) = decomp_DLAMV_name la ldef in
+            let vlna = Array.of_list lna 
+            in 
+	    if (array_for_all (noccur_with_meta evd n nbfix) varit) then
+              (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs)
+              &&
+              (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) 
+            else 
+	      error "Recursive call in the type of a declaration"
+		
+	| (DOPN(MutCase _,_) as mc,l) -> 
+            let (_,p,c,vrest) = destCase mc in
+            if (noccur_with_meta evd n nbfix p) then
+              if (noccur_with_meta evd n nbfix c) then
+		if (List.for_all (noccur_with_meta evd n nbfix) l) then
+		  (array_for_all (check_rec_call alreadygrd n vlra) vrest)
+		else 
+		  error "Recursive call in the argument of a function defined by cases"        
+              else 
+		error "Recursive call in the argument of a case expression"
+            else 
+	      error "Recursive call in the type of a Case expression" 
+              
+	| _    -> error "Definition not in guarded form"
+	      
+  in 
+  check_rec_call false 1 vlra def
+
+(* The  function which checks that the whole block of definitions 
+   satisfies the guarded condition *)
+
+let check_cofix env f = 
+  match f with
+    | DOPN(CoFix(j),vargs) -> 
+	let nbfix = let nv = Array.length vargs in 
+        if nv < 2 then
+          error "Ill-formed recursive definition" 
+        else 
+	  nv-1 
+	in
+	let varit = Array.sub vargs 0 nbfix in
+	let ldef  = array_last vargs in
+	let la    = Array.length varit in
+	let (lna,vdefs) = decomp_DLAMV_name la ldef in
+	let vlna = Array.of_list lna in
+	let check_type i = 
+	  (try 
+	     let _ = check_guard_rec_meta env nbfix vdefs.(i) varit.(i) in ()
+	   with UserError (s,str) -> 
+	     error_ill_formed_rec_body str CCI env lna i vdefs) 
+	in
+	for i = 0 to nbfix-1 do check_type i done
+    | _ -> assert false
+
+(* Checks the type of a (co)fixpoint.
+   Fix and CoFix are typed the same way; only the guard condition differs. *)
+
+exception IllBranch of int
+
+let type_fixpoint env lna lar vdefj =
+  let lt = Array.length vdefj in
+  assert (Array.length lar = lt);
+  try
+    let cv = 
+      conv_forall2_i
+	(fun i e def ar -> 
+	   let c = conv_leq e def (lift lt ar) in
+	   if c = NotConvertible then raise (IllBranch i) else c)
+	env (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
+    in
+    begin match cv with
+      | Convertible g -> g
+      | NotConvertible -> assert false
+    end
+  with IllBranch i ->
+    error_ill_typed_rec_body CCI env i lna vdefj lar
diff --git a/kernel/machops.mli b/kernel/machops.mli
index c59d3344d8..d0fa5eb5c9 100644
--- a/kernel/machops.mli
+++ b/kernel/machops.mli
@@ -10,42 +10,40 @@ open Environ
 
 (* 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
 
+val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type
 
 (* 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_constant_or_existential : 'a unsafe_env -> constr -> typed_type
 
-val type_of_mind : 'a unsafe_env -> constr -> typed_type
+val type_of_inductive : 'a unsafe_env -> constr -> typed_type
 
-val type_of_mconstr : 'a unsafe_env -> constr -> typed_type
+val type_of_constructor : 'a unsafe_env -> constr -> constr
 
 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_prop_or_set : 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
+  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+    -> unsafe_judgment * universes
 
 val gen_rel :
-  'a unsafe_env -> name -> typed_type -> unsafe_judgment -> unsafe_judgment
+  'a unsafe_env -> name -> typed_type -> unsafe_judgment 
+    -> unsafe_judgment * universes
 
 val cast_rel : 
   'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
diff --git a/kernel/printer.mli b/kernel/printer.mli
index f737f0ced4..d9c2336bc2 100644
--- a/kernel/printer.mli
+++ b/kernel/printer.mli
@@ -2,7 +2,15 @@
 (* $Id$ *)
 
 open Pp
+open Names
 open Term
+open Sign
+open Environ
 
-val prterm : constr -> std_ppcmds
+val pr_id : identifier -> std_ppcmds
+val pr_sp : section_path -> std_ppcmds
+
+val gen_pr_term : path_kind -> 'a unsafe_env -> constr -> std_ppcmds
+val pr_term : constr -> std_ppcmds
+val pr_ne_env : std_ppcmds -> path_kind -> environment -> std_ppcmds
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 06f973ff62..b78dab085e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -171,8 +171,8 @@ let subst_term_occ locs c t =
     if List.exists (fun o -> o>=nbocc or o<= -nbocc) locs then
       errorlabstrm "subst_occ" 
 	[< 'sTR "Only "; 'iNT (nbocc-1); 'sTR " occurrences of";
-	   'bRK(1,1); Printer.prterm c; 'sPC;
-	   'sTR "in"; 'bRK(1,1); Printer.prterm t>]
+	   'bRK(1,1); Printer.pr_term c; 'sPC;
+	   'sTR "in"; 'bRK(1,1); Printer.pr_term t>]
     else 
       t'
 
@@ -792,6 +792,13 @@ let sort_cmp pb s0 s1 =
 	   | CONV_LEQ -> convert_of_constraint (enforce_geq u2 u1))
     | (_, _) -> fun _ -> NotConvertible
 
+let base_sort_cmp pb s0 s1 =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) -> c1 = c2
+    | (Prop c1, Type u)  -> not (pb_is_equal pb)
+    | (Type u1, Type u2) -> true
+    | (_, _) -> false
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 
 let rec ccnv cv_pb infos lft1 lft2 term1 term2 = 
@@ -930,8 +937,38 @@ let fconv cv_pb env t1 t2 =
     let infos = create_clos_infos hnf_flags env in
     ccnv cv_pb infos ELID ELID (inject t1) (inject t2) univ
 
-let conv       env term1 term2 = fconv CONV env term1 term2
-let conv_leq   env term1 term2 = fconv CONV_LEQ env term1 term2
+let conv env term1 term2 = fconv CONV env term1 term2
+let conv_leq env term1 term2 = fconv CONV_LEQ env term1 term2
+
+let conv_forall2 f env v1 v2 =
+  let (_,c) =
+    array_fold_left2 
+      (fun a x y -> match a with
+	 | (_,NotConvertible) -> a
+	 | (e,Convertible u) -> let e' = set_universes u env in (e',f e x y))
+      (env, Convertible (universes env)) 
+      v1 v2
+  in
+  c
+
+let conv_forall2_i f env v1 v2 =
+  let (_,c) =
+    array_fold_left2_i 
+      (fun i a x y -> match a with
+	 | (_,NotConvertible) -> a
+	 | (e,Convertible u) -> let e' = set_universes u env in (e',f i e x y))
+      (env, Convertible (universes env)) 
+      v1 v2
+  in
+  c
+
+let test_conversion f env x y =
+  match f env x y with
+    | Convertible _ -> true
+    | NotConvertible -> false
+
+let is_conv env = test_conversion conv env
+let is_conv_leq env = test_conversion conv_leq env
 
 
 (********************************************************************)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index d34a0d99d3..7d3dd44b7a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -156,6 +156,7 @@ type conversion_result =
 type conversion_test = universes -> conversion_result
 
 val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
+val base_sort_cmp : conv_pb -> sorts -> sorts -> bool
 
 val bool_and_convert : bool -> conversion_test -> conversion_test
 val convert_and : conversion_test -> conversion_test -> conversion_test
@@ -178,6 +179,16 @@ val fconv : conv_pb -> 'a conversion_function
 val conv : 'a conversion_function
 val conv_leq : 'a conversion_function
 
+val conv_forall2 : 
+  'a conversion_function -> 'a unsafe_env 
+    -> constr array -> constr array -> conversion_result
+
+val conv_forall2_i : 
+  (int -> 'a conversion_function) -> 'a unsafe_env 
+    -> constr array -> constr array -> conversion_result
+
+val is_conv : 'a unsafe_env -> constr -> constr -> bool
+val is_conv_leq : 'a unsafe_env -> constr -> constr -> bool
 
 (*s Obsolete Reduction Functions *)
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 923c91d03c..661f64042c 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -235,3 +235,4 @@ let lookup_id id env =
 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 151be2029c..ebf98a8f41 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -80,3 +80,4 @@ val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
 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 87cc1aaaec..a662f74392 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -61,6 +61,10 @@ type typed_term = typed_type judge
 
 let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
+let body_of_type ty = ty.body
+
+let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 82c54f0bbf..ee60fbedde 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -58,6 +58,10 @@ type typed_term = typed_type judge
 
 val typed_app : (constr -> constr) -> typed_type -> typed_type
 
+val body_of_type : typed_type -> constr
+
+val incast_type : typed_type -> constr
+
 (*s Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the 
   manipulation of terms. Some of these functions may be overlapped with
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e20a1f0677..203b0cbc6a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -17,6 +17,8 @@ val initial_universes : universes
 
 val super : universe -> universes -> universe * universes
 
+val sup : universe -> universe -> universes -> universe * universes
+
 type constraint_result = 
   | Consistent of universes
   | Inconsistent