module Reduction (fin)

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

7 files changed, 1060 insertions, 946 deletions

diff --git a/kernel/constant.mli b/kernel/constant.mli
index 5c6fb0d139..4de51f8593 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -1,4 +1,20 @@
 
 (* $Id$ *)
 
-type constant
+open Names
+open Term
+
+type discharge_recipe
+
+type recipe =
+  | Cooked of constr
+  | Recipe of discharge_recipe
+
+type constant_body = {
+  const_kind : path_kind;
+  const_body : recipe ref option;
+  const_type : type_judgment;
+  mutable const_eval : ((int * constr) list * int * bool) option option;
+}
+
+type constant_entry = section_path * constant_body
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 485d1baa3f..cc579f3509 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -3,12 +3,14 @@
 
 open Names
 open Sign
+open Univ
 open Term
 
 type 'a unsafe_env = {
   context : context;
   sigma : 'a evar_map;
-  metamap : (int * constr) list
+  metamap : (int * constr) list;
+  constraints : universes
 }
   
 (* First character of a constr *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 98d9e7b88f..af2a131943 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -5,20 +5,26 @@ open Names
 open Term
 open Constant
 open Inductive
+open Evd
 open Univ
 
 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 push_var : identifier * constr -> 'a unsafe_env -> 'a unsafe_env
 val push_rel : name * constr -> 'a unsafe_env -> 'a unsafe_env
 
-val add_constant : constant -> 'a unsafe_env -> 'a unsafe_env
-val add_mind : mind -> '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_constant : section_path -> 'a unsafe_env -> constant
+val lookup_constant : section_path -> 'a unsafe_env -> constant_entry
 
 val id_of_global : 'a unsafe_env -> sorts oper -> identifier
 val id_of_name_using_hdchar : 'a unsafe_env -> constr -> name -> identifier
@@ -28,15 +34,18 @@ val translucent_abst : 'a unsafe_env -> constr -> bool
 val evaluable_abst : 'a unsafe_env -> constr -> bool
 val abst_value : 'a unsafe_env -> constr -> constr
 
+val defined_const : 'a unsafe_env -> constr -> bool
 val translucent_const : 'a unsafe_env -> constr -> bool
 val evaluable_const : 'a unsafe_env -> constr -> bool
 val const_value : 'a unsafe_env -> constr -> constr
+val const_type : 'a unsafe_env -> constr -> constr
+val const_of_path : 'a unsafe_env -> section_path -> constant_entry
+
+val is_existential : constr -> bool
 
 val const_abst_opt_value : 'a unsafe_env -> constr -> constr option
 
+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
-
-val sort_cmp : 'a unsafe_env -> conv_pb -> sorts -> sorts -> bool * universes
-
-
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 17c89ac93d..32d844e9a7 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,4 +1,12 @@
 
 (* $Id$ *)
 
-type mind
+open Names
+
+type mind_entry
+
+type mutual_inductive_body
+
+type mutual_inductive_entry = section_path * mutual_inductive_body
+
+val mind_type_finite : mutual_inductive_body -> int -> bool
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5b88d5e69f..5636bbbc81 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -8,6 +8,8 @@ open Generic
 open Term
 open Univ
 open Evd
+open Constant
+open Inductive
 open Environ
 open Closure
 
@@ -25,37 +27,39 @@ type 'a stack_reduction_function = 'a unsafe_env -> constr -> constr list
 (*** Reduction Functions Operators ***)
 (*************************************)
 
-let rec under_casts f = function
-  | DOP2(Cast,c,t) -> DOP2(Cast,under_casts f c, t)
-  | c              -> f c
+let rec under_casts f env = function
+  | DOP2(Cast,c,t) -> DOP2(Cast,under_casts f env c, t)
+  | c              -> f env c
 
-let rec whd_stack x stack =
+let rec whd_stack env x stack =
   match x with
-    | DOPN(AppL,cl)  -> whd_stack cl.(0) (array_app_tl cl stack)
-    | DOP2(Cast,c,_) -> whd_stack c stack
+    | DOPN(AppL,cl)  -> whd_stack env cl.(0) (array_app_tl cl stack)
+    | DOP2(Cast,c,_) -> whd_stack env c stack
     | _              -> (x,stack)
 	  
-let stack_reduction_of_reduction red_fun x stack =
-  let t = red_fun (applistc x stack) in
-  whd_stack t []
+let stack_reduction_of_reduction red_fun env x stack =
+  let t = red_fun env (applistc x stack) in
+  whd_stack env t []
 
-let rec strong whdfun t = 
-  match whdfun t with 
+let strong whdfun env = 
+  let rec strongrec = function
     | DOP0 _ as t -> t
-	(* Cas ad hoc *)
-    | DOP1(oper,c) -> DOP1(oper,strong whdfun c)
-    | DOP2(oper,c1,c2) -> DOP2(oper,strong whdfun c1,strong whdfun c2)
-    | DOPN(oper,cl) -> DOPN(oper,Array.map (strong whdfun) cl)
-    | DOPL(oper,cl) -> DOPL(oper,List.map (strong whdfun) cl)
-    | DLAM(na,c) -> DLAM(na,strong whdfun c)
-    | DLAMV(na,c) -> DLAMV(na,Array.map (strong whdfun) c)
+    (* Cas ad hoc *)
+    | DOP1(oper,c) -> DOP1(oper,strongrec c)
+    | DOP2(oper,c1,c2) -> DOP2(oper,strongrec c1,strongrec c2)
+    | DOPN(oper,cl) -> DOPN(oper,Array.map strongrec cl)
+    | DOPL(oper,cl) -> DOPL(oper,List.map strongrec cl)
+    | DLAM(na,c) -> DLAM(na,strongrec c)
+    | DLAMV(na,c) -> DLAMV(na,Array.map strongrec c)
     | VAR _ as t -> t
     | Rel _ as t -> t
+  in
+  strongrec
 
-let rec strong_prodspine redfun c = 
-  match redfun c with
+let rec strong_prodspine redfun env c = 
+  match redfun env c with
     | DOP2(Prod,a,DLAM(na,b)) ->
-        DOP2(Prod,a,DLAM(na,strong_prodspine redfun b))
+        DOP2(Prod,a,DLAM(na,strong_prodspine redfun env b))
     | x -> x
 
 
@@ -89,17 +93,6 @@ let nf_betadeltaiota env =  clos_norm_flags betadeltaiota env
 let whd_flags flgs env t =
   whd_val (create_clos_infos flgs env) (inject t)
 
-(*
-let whd_beta = whd_flags beta mt_evd
-let whd_betaiota = whd_flags betaiota mt_evd
-let whd_betadeltaiota = whd_flags betadeltaiota
-
-let whd_beta_stack = stack_reduction_of_reduction whd_beta
-let whd_betaiota_stack = stack_reduction_of_reduction whd_betaiota
-let whd_betadeltaiota_stack env = 
-  stack_reduction_of_reduction (whd_betadeltaiota env)
-*)
-
 
 (* Red reduction tactic: reduction to a product *)
 let red_product env c = 
@@ -121,144 +114,170 @@ let red_product env c =
    the list may contain only negative occurrences that will not be substituted *)
 (* Aurait sa place dans term.ml mais term.ml ne connait pas printer.ml *)
 let subst_term_occ locs c t = 
- let rec substcheck except k occ c t =
-        if except or List.exists (function u -> u>=occ) locs 
-        then substrec except k occ c t
-        else (occ,t)
-and substrec except k occ c t =
-   if eq_constr t c then
-     if except then if List.mem (-occ) locs then (occ+1,t)
-     else (occ+1,Rel(k))
-     else if List.mem occ locs then  (occ+1,Rel(k))
-     else  (occ+1,t)
-   else match t with
-     DOPN(Const sp,tl) -> occ,t
-  |  DOPN(MutConstruct _,tl) -> occ,t
-  |  DOPN(MutInd _,tl) -> occ,t
-
-  |  DOPN(i,cl) -> let (occ',cl') =   
-                        Array.fold_left (fun (nocc',lfd) f ->
-                         let (nocc'',f') = substcheck except k nocc' c f
-                         in (nocc'',f'::lfd)) (occ,[]) cl
-                        in (occ',DOPN(i,Array.of_list (List.rev cl')))
-
-  |  DOP2(i,t1,t2) -> let (nocc1,t1')=substrec except k occ c t1 in
-                        let (nocc2,t2')=substcheck except k nocc1 c t2
-                        in nocc2,DOP2(i,t1',t2')
-  |  DOP1(i,t)  -> let (nocc,t')= substrec except k occ c t in
-                        nocc,DOP1(i,t')
-
-  |  DLAM(n,t)        -> let (occ',t') = substcheck except (k+1) occ (lift 1 c) t
-                        in (occ',DLAM(n,t'))
-
-  |  DLAMV(n,cl)      -> let (occ',cl') =   
-                        Array.fold_left (fun (nocc',lfd) f ->
-                         let (nocc'',f') = substcheck except (k+1) nocc' (lift 1 c) f
-                         in (nocc'',f'::lfd)) (occ,[]) cl
-                        in (occ',DLAMV(n,Array.of_list (List.rev cl') ))
-  |  _               -> occ,t
- in if locs = [] then subst_term c t
-    else if List.mem 0 locs then t
-    else let except = List.for_all (fun n -> n<0) locs in
-	 let (nbocc,t') = substcheck except 1 1 c t in
-	   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>]
-	   else t'
-
+  let rec substcheck except k occ c t =
+    if except or List.exists (function u -> u>=occ) locs then
+      substrec except k occ c t
+    else 
+      (occ,t)
+  and substrec except k occ c t =
+    if eq_constr t c then
+      if except then 
+	if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
+      else 
+	if List.mem occ locs then (occ+1,Rel(k)) else  (occ+1,t)
+    else 
+      match t with
+	| DOPN(Const sp,tl) -> occ,t
+	|  DOPN(MutConstruct _,tl) -> occ,t
+	|  DOPN(MutInd _,tl) -> occ,t
+	|  DOPN(i,cl) -> 
+	     let (occ',cl') =   
+               Array.fold_left 
+		 (fun (nocc',lfd) f ->
+		    let (nocc'',f') = substcheck except k nocc' c f in
+                    (nocc'',f'::lfd)) 
+		 (occ,[]) cl
+             in 
+	     (occ',DOPN(i,Array.of_list (List.rev cl')))
+	|  DOP2(i,t1,t2) -> 
+	     let (nocc1,t1')=substrec except k occ c t1 in
+             let (nocc2,t2')=substcheck except k nocc1 c t2 in
+             nocc2,DOP2(i,t1',t2')
+	|  DOP1(i,t) -> 
+	     let (nocc,t')= substrec except k occ c t in
+	     nocc,DOP1(i,t')
+	|  DLAM(n,t) -> 
+	     let (occ',t') = substcheck except (k+1) occ (lift 1 c) t in
+             (occ',DLAM(n,t'))
+	|  DLAMV(n,cl) -> 
+	     let (occ',cl') =   
+               Array.fold_left 
+		 (fun (nocc',lfd) f ->
+		    let (nocc'',f') = 
+		      substcheck except (k+1) nocc' (lift 1 c) f
+                    in (nocc'',f'::lfd)) 
+		 (occ,[]) cl
+             in 
+	     (occ',DLAMV(n,Array.of_list (List.rev cl') ))
+	|  _               -> occ,t
+  in 
+  if locs = [] then 
+    subst_term c t
+  else if List.mem 0 locs then 
+    t
+  else 
+    let except = List.for_all (fun n -> n<0) locs in
+    let (nbocc,t') = substcheck except 1 1 c t in
+    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>]
+    else 
+      t'
 
 (* linear substitution (following pretty-printer) of the value of name in c.
  * n is the number of the next occurence of name.
  * ol is the occurence list to find. *)
 let rec substlin env name n ol c =
   match c with
-      DOPN(Const sp,_) ->
+    | DOPN(Const sp,_) ->
         if (path_of_const c)=name then
           if (List.hd ol)=n then
-            if evaluable_const env c then ((n+1),(List.tl ol), const_value env c)
+            if evaluable_const env c then 
+	      ((n+1),(List.tl ol), const_value env c)
             else
               errorlabstrm "substlin"
                 [< 'sTR(string_of_path sp);
                    'sTR " is not a defined constant" >]
-          else ((n+1),ol,c)
-        else (n,ol,c)
+          else 
+	    ((n+1),ol,c)
+        else 
+	  (n,ol,c)
 
     | DOPN(Abst _,_) ->
         if (path_of_abst c)=name then
-          if (List.hd ol)=n then ((n+1),(List.tl ol), abst_value env c)
-          else ((n+1),ol,c)
-        else (n,ol,c)
+          if (List.hd ol)=n then 
+	    ((n+1),(List.tl ol), abst_value env c)
+          else 
+	    ((n+1),ol,c)
+        else 
+	  (n,ol,c)
 
 (* INEFFICIENT: OPTIMIZE *)
     | DOPN(AppL,tl) ->
         let c1 = array_hd tl and cl = array_tl tl in
-          Array.fold_left (fun (n1,ol1,c1') c2 ->
-                     (match ol1 with 
-                          [] -> (n1,[],applist(c1',[c2]))
-                        | _  ->
-                            let (n2,ol2,c2') = substlin env name n1 ol1 c2
-                            in (n2,ol2,applist(c1',[c2']))))
-            (substlin env name n ol c1) cl
+        Array.fold_left 
+	  (fun (n1,ol1,c1') c2 ->
+	     (match ol1 with 
+                | [] -> (n1,[],applist(c1',[c2]))
+                | _  ->
+                    let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
+                    (n2,ol2,applist(c1',[c2']))))
+          (substlin env name n ol c1) cl
 
     | DOP2(Lambda,c1,DLAM(na,c2)) ->
-        let (n1,ol1,c1') = substlin env name n ol c1
-        in (match ol1 with 
-                [] -> (n1,[],DOP2(Lambda,c1',DLAM(na,c2)))
-              | _  ->
-                  let (n2,ol2,c2') = substlin env name n1 ol1 c2
-                  in (n2,ol2,DOP2(Lambda,c1',DLAM(na,c2'))))
-    | DOP2(Prod,c1,DLAM(na,c2))   ->
-        let (n1,ol1,c1') = substlin env name n ol c1
-        in (match ol1 with 
-                [] -> (n1,[],DOP2(Prod,c1',DLAM(na,c2)))
-              | _  ->
-                  let (n2,ol2,c2') = substlin env name n1 ol1 c2
-                  in (n2,ol2,DOP2(Prod,c1',DLAM(na,c2'))))
-    | DOPN(MutCase _,_)   -> let (ci,p,d,llf) = destCase c in
+        let (n1,ol1,c1') = substlin env name n ol c1 in
+        (match ol1 with 
+           | [] -> (n1,[],DOP2(Lambda,c1',DLAM(na,c2)))
+           | _  ->
+               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
+               (n2,ol2,DOP2(Lambda,c1',DLAM(na,c2'))))
+
+    | DOP2(Prod,c1,DLAM(na,c2)) ->
+        let (n1,ol1,c1') = substlin env name n ol c1 in
+        (match ol1 with 
+           | [] -> (n1,[],DOP2(Prod,c1',DLAM(na,c2)))
+           | _  ->
+               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
+               (n2,ol2,DOP2(Prod,c1',DLAM(na,c2'))))
+	
+    | DOPN(MutCase _,_) -> 
+	let (ci,p,d,llf) = destCase c in
         let rec substlist nn oll = function
-            []     -> (nn,oll,[])
+          | []     -> (nn,oll,[])
           | f::lfe ->
               let (nn1,oll1,f') = substlin env name nn oll f in
               (match oll1 with
-                   [] -> (nn1,[],f'::lfe)
+                 | [] -> (nn1,[],f'::lfe)
                  | _  ->
-                    let (nn2,oll2,lfe') = substlist nn1 oll1 lfe 
-                    in (nn2,oll2,f'::lfe'))
-       in
-       let (n1,ol1,p') = substlin env name n ol p in  (* ATTENTION ERREUR *)
+                     let (nn2,oll2,lfe') = substlist nn1 oll1 lfe in
+                     (nn2,oll2,f'::lfe'))
+	in
+	let (n1,ol1,p') = substlin env name n ol p in  (* ATTENTION ERREUR *)
         (match ol1 with                                 (* si P pas affiche *)
-           [] -> (n1,[],mkMutCaseA ci p' d llf)
-         | _  ->
-           let (n2,ol2,d') = substlin env name n1 ol1 d in
-           (match ol2 with
-              [] -> (n2,[],mkMutCaseA ci p' d' llf)
-            | _  -> 
-	        let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf)
-                in (n3,ol3,mkMutCase ci p' d' lf')))
+           | [] -> (n1,[],mkMutCaseA ci p' d llf)
+           | _  ->
+               let (n2,ol2,d') = substlin env name n1 ol1 d in
+               (match ol2 with
+		  | [] -> (n2,[],mkMutCaseA ci p' d' llf)
+		  | _  -> 
+	              let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf)
+                      in (n3,ol3,mkMutCase ci p' d' lf')))
         
     | DOP2(Cast,c1,c2)   ->
-        let (n1,ol1,c1') = substlin env name n ol c1
-        in (match ol1 with 
-                [] -> (n1,[],DOP2(Cast,c1',c2))
-              | _  ->
-                  let (n2,ol2,c2') = substlin env name n1 ol1 c2
-                  in (n2,ol2,DOP2(Cast,c1',c2')))
+        let (n1,ol1,c1') = substlin env name n ol c1 in
+        (match ol1 with 
+           | [] -> (n1,[],DOP2(Cast,c1',c2))
+           | _  ->
+               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
+               (n2,ol2,DOP2(Cast,c1',c2')))
+
     | DOPN(Fix _,_) -> 
         (warning "do not consider occurrences inside fixpoints"; (n,ol,c))
-
+	
     | DOPN(CoFix _,_) -> 
         (warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
-
+	
     | _ -> (n,ol,c)
-
-
+	  
 let unfold env name =
-  let flag = (UNIFORM,{ r_beta = true;
-                        r_delta = (fun op -> op=(Const name) or op=(Abst name));
-                        r_iota = true })
-  in clos_norm_flags flag env
+  let flag = 
+    (UNIFORM,{ r_beta = true;
+               r_delta = (fun op -> op=(Const name) or op=(Abst name));
+               r_iota = true })
+  in 
+  clos_norm_flags flag env
 
 
 (* unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)
@@ -267,34 +286,31 @@ let unfold env name =
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env (occl,name) c =
   match occl with
-      []  -> unfold env name c
+    | []  -> unfold env name c
     | l -> 
         match substlin env name 1 (Sort.list (<) l) c with
-            (_,[],uc) -> nf_betaiota env uc
+          | (_,[],uc) -> nf_betaiota env uc
           | (1,_,_) -> error ((string_of_path name)^" does not occur")
           | _ -> error ("bad occurrence numbers of "^(string_of_path name))
 
-
 (* Unfold reduction tactic: *)
 let unfoldn loccname env c = 
   List.fold_left (fun c occname -> unfoldoccs env occname c) c loccname
 
-
-
 (* Re-folding constants tactics: refold com in term c *)
-let fold_one_com env com c =
+let fold_one_com com env c =
   let rcom = red_product env com in
   subst1 com (subst_term rcom c)
 
 let fold_commands cl env c =
-  List.fold_right (fold_one_com env) (List.rev cl) c
+  List.fold_right (fun com -> fold_one_com com env) (List.rev cl) c
 
 
 (* Pattern *)
-(* 
- * gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
- * the specified occurrences.
- *)
+
+(* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
+ * the specified occurrences. *)
+
 let abstract_scheme env (locc,a,ta) t =
   let na = named_hd env ta Anonymous in
   if occur_meta ta then
@@ -305,9 +321,9 @@ let abstract_scheme env (locc,a,ta) t =
     DOP2(Lambda, ta, DLAM(na,subst_term_occ locc a t))
 
 
-let pattern_occs env loccs_trm_typ c =
+let pattern_occs loccs_trm_typ env c =
   let abstr_trm = List.fold_right (abstract_scheme env) loccs_trm_typ c in
-    applist(abstr_trm, List.map (fun (_,t,_) -> t) loccs_trm_typ)
+  applist(abstr_trm, List.map (fun (_,t,_) -> t) loccs_trm_typ)
 
 
 (*************************************)
@@ -318,7 +334,7 @@ let pattern_occs env loccs_trm_typ c =
 
 let rec stacklam recfun env t stack =
   match (stack,t) with
-    | ((h::stacktl), (DOP2(Lambda,_,DLAM(_,c)))) ->
+    | (h::stacktl, DOP2(Lambda,_,DLAM(_,c))) ->
         stacklam recfun (h::env) c stacktl
     | _ -> recfun (substl env t) stack
 
@@ -326,85 +342,71 @@ let rec stacklam recfun env t stack =
 let beta_applist (c,l) = stacklam (fun c l -> applist(c,l)) [] c l
 
 
-let whd_beta_stack = 
- let rec whrec x stack = match x with
-    DOP2(Lambda,c1,DLAM(name,c2)) ->
-      (match stack with
-         []       -> (x,[])
-       | a1::rest -> stacklam whrec [a1] c2 rest)
-
-  | DOPN(AppL,cl)  -> whrec (array_hd cl) (array_app_tl cl stack)
-  | DOP2(Cast,c,_) -> whrec c stack
-  | x              -> (x,stack)
- in whrec
-  
-
-
-let whd_beta x = applist(whd_beta_stack x [])
-
-(***
-let whd_betaimplicit_stack = whrec
-    where rec whrec x stack =
-    match x with
-    DOP2(Lambda,DOP0(Implicit),DLAM(name,c2)) ->
-    (match stack with
-     [] -> x,[]
-   | a1::rest -> stacklam (fun l x -> whrec x l)[a1] rest c2)
-
-  | DOPN(AppL,cl)      -> whrec (hd_vect cl) (app_tl_vect cl stack)
-  | DOP2(Cast,c,_)       ->  whrec c stack
-  | x -> x,stack
-
+let whd_beta_stack env = 
+  let rec whrec x stack = match x with
+    | DOP2(Lambda,c1,DLAM(name,c2)) ->
+	(match stack with
+           | [] -> (x,[])
+	   | a1::rest -> stacklam whrec [a1] c2 rest)
+	
+    | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
+    | DOP2(Cast,c,_) -> whrec c stack
+    | x -> (x,stack)
+  in 
+  whrec
 
-let whd_betaimplicit x = applist(whd_betaimplicit_stack x [])
-***)
+let whd_beta env x = applist (whd_beta_stack env x [])
 
 
 (* 2. Delta Reduction *)
-
+		   
 let whd_const_stack namelist env = 
- let rec whrec x l =
+  let rec whrec x l =
     match x with
-    (DOPN(Const sp,_)) as c      ->
-    if List.mem sp namelist then
-        if evaluable_const env c then
-            whrec (const_value env c) l
-        else error "whd_const_stack"
-    else x,l
-
-  | (DOPN(Abst sp,_)) as c      ->
-    if List.mem sp namelist then
-        if evaluable_abst env c then
-            whrec (abst_value env c) l
-        else error "whd_const_stack"
-    else x,l
-
-  | DOP2(Cast,c,_) -> whrec c l
-  | DOPN(AppL,cl)    -> whrec (array_hd cl) (array_app_tl cl l)
-  | x             -> x,l
- in whrec
-    
+      | DOPN(Const sp,_) as c ->
+	  if List.mem sp namelist then
+            if evaluable_const env c then
+              whrec (const_value env c) l
+            else 
+	      error "whd_const_stack"
+	  else 
+	    x,l
+
+      | (DOPN(Abst sp,_)) as c ->
+	  if List.mem sp namelist then
+            if evaluable_abst env c then
+              whrec (abst_value env c) l
+            else 
+	      error "whd_const_stack"
+	  else 
+	    x,l
+	      
+      | DOP2(Cast,c,_) -> whrec c l
+      | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l)
+      | x -> x,l
+  in 
+  whrec
 
 let whd_const namelist env c = applist(whd_const_stack namelist env c [])
 
-
 let whd_delta_stack env = 
- let rec whrec x l =
+  let rec whrec x l =
     match x with
-    (DOPN(Const _,_)) as c      ->
-    if evaluable_const env c then
-           whrec (const_value env c) l
-    else x,l
-  | (DOPN(Abst _,_)) as c      ->
-    if evaluable_abst env c then
-           whrec (abst_value env c) l
-    else x,l
-
+      | DOPN(Const _,_) as c ->
+	  if evaluable_const env c then
+            whrec (const_value env c) l
+	  else 
+	    x,l
+      | (DOPN(Abst _,_)) as c ->
+	  if evaluable_abst env c then
+            whrec (abst_value env c) l
+	  else 
+	    x,l
   | DOP2(Cast,c,_) -> whrec c l
-  | DOPN(AppL,cl)    -> whrec (array_hd cl) (array_app_tl cl l)
-  | x             -> x,l
- in whrec
-    
+  | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l)
+  | x -> x,l
+  in 
+  whrec
 
 let whd_delta env c = applist(whd_delta_stack env c [])
 
@@ -412,23 +414,25 @@ let whd_delta env c = applist(whd_delta_stack env c [])
 let whd_betadelta_stack env = 
   let rec whrec x l =
     match x with
-        DOPN(Const _,_) ->
-          if evaluable_const env x then whrec (const_value env x) l
-          else (x,l)
+      | DOPN(Const _,_) ->
+          if evaluable_const env x then 
+	    whrec (const_value env x) l
+          else 
+	    (x,l)
       | DOPN(Abst _,_) ->
-          if evaluable_abst env x then whrec (abst_value env x) l
-          else (x,l)
-
+          if evaluable_abst env x then 
+	    whrec (abst_value env x) l
+          else 
+	    (x,l)
       | DOP2(Cast,c,_) -> whrec c l
       | DOPN(AppL,cl)  -> whrec (array_hd cl) (array_app_tl cl l)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match l with
-               [] -> (x,l)
+             | [] -> (x,l)
              | (a::m) -> stacklam whrec [a] c m)
       | x -> (x,l)
-
-  in whrec
-
+  in 
+  whrec
 
 let whd_betadelta env c = applist(whd_betadelta_stack env c [])
 
@@ -436,101 +440,98 @@ let whd_betadelta env c = applist(whd_betadelta_stack env c [])
 let whd_betadeltat_stack env = 
   let rec whrec x l =
     match x with
-        DOPN(Const _,_) ->
-          if translucent_const env x then whrec (const_value env x) l
-          else (x,l)
-
+      | DOPN(Const _,_) ->
+          if translucent_const env x then 
+	    whrec (const_value env x) l
+          else 
+	    (x,l)
       | DOPN(Abst _,_) ->
-          if translucent_abst env x then whrec (abst_value env x) l
-          else (x,l)
-
+          if translucent_abst env x then 
+	    whrec (abst_value env x) l
+          else 
+	    (x,l)
       | DOP2(Cast,c,_) -> whrec c l
-      | DOPN(AppL,cl)    -> whrec (array_hd cl) (array_app_tl cl l)
+      | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match l with
-               [] -> (x,l)
+             | [] -> (x,l)
              | (a::m) -> stacklam whrec [a] c m)
       | x -> (x,l)
-
-  in whrec
-
-
+  in 
+  whrec
+       
 let whd_betadeltat env c = applist(whd_betadeltat_stack env c [])
 
-
 let whd_betadeltaeta_stack env = 
   let rec whrec x stack =
     match x with
-        DOPN(Const _,_) ->
-          if evaluable_const env x then whrec (const_value env x) stack
-          else (x,stack)
+      | DOPN(Const _,_) ->
+          if evaluable_const env x then
+	    whrec (const_value env x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
-          if evaluable_abst env x then whrec (abst_value env x) stack
-          else (x,stack)
-
+          if evaluable_abst env x then
+	    whrec (abst_value env x) stack
+          else 
+	    (x,stack)
       | DOP2(Cast,c,_) -> whrec c stack
       | DOPN(AppL,cl)    -> whrec (array_hd cl) (array_app_tl cl stack)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with
-               [] -> (match applist (whrec c []) with 
-                          (DOPN(AppL,cl)) -> 
-                            (match whrec (array_last cl) [] with 
-                                 (Rel 1,[]) -> let napp = (Array.length cl) -1 in
-                                   if napp = 0 then (x,stack) else
-                                     let lc = Array.sub cl 0 napp in
-                                     let u = if napp = 1 then lc.(0) else DOPN(AppL,lc) 
-                                     in if noccurn 1 u then (pop u,[]) else (x,stack)
-                               | _ -> (x,stack))
-                        | _ -> (x,stack))
+             | [] -> 
+		 (match applist (whrec c []) with 
+                    | DOPN(AppL,cl) -> 
+                        (match whrec (array_last cl) [] with 
+                           | (Rel 1,[]) -> 
+			       let napp = (Array.length cl) -1 in
+                               if napp = 0 then (x,stack) else
+                                 let lc = Array.sub cl 0 napp in
+                                 let u = 
+				   if napp = 1 then lc.(0) else DOPN(AppL,lc) 
+                                 in 
+				 if noccurn 1 u then (pop u,[]) else (x,stack)
+                           | _ -> (x,stack))
+                    | _ -> (x,stack))
              | (a::m) -> stacklam whrec [a] c m)
-
-  | x -> (x,stack)
- 
-  in whrec
-
+      | x -> (x,stack)
+  in 
+  whrec
 
 let whd_betadeltaeta env x = applist(whd_betadeltaeta_stack env x [])
 
-
-
 (* 3. Iota reduction *)
 
-type 'a miota_args =
-    {mP      : constr;   (* the result type *)
-     mconstr : constr;   (* the constructor *)
-     mci     : case_info;  (* special info to re-build pattern *)
-     mcargs  : 'a list;  (* the constructor's arguments *)
-     mlf     : 'a array} (* the branch code vector *)
-
-
+type 'a miota_args = {
+  mP      : constr;     (* the result type *)
+  mconstr : constr;     (* the constructor *)
+  mci     : case_info;  (* special info to re-build pattern *)
+  mcargs  : 'a list;    (* the constructor's arguments *)
+  mlf     : 'a array }  (* the branch code vector *)
+		       
 let reducible_mind_case c =
   match c with 
-      DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
+    | DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
     | _  -> false
 
-
-
 let contract_cofix = function
   | DOPN(CoFix(bodynum),bodyvect) ->
       let nbodies = (Array.length bodyvect) -1 in
       let make_Fi j = DOPN(CoFix(j),bodyvect) in
-    	sAPPViList bodynum (array_last bodyvect) 
-	  (list_tabulate make_Fi nbodies)
+      sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
   | _ -> assert false
 
-
 let reduce_mind_case env mia =
   match mia.mconstr with 
-     (DOPN(MutConstruct((indsp,tyindx),i),_)) ->
-       let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
-       let nparams    = mind_nparams env ind in
-       let real_cargs = snd (list_chop nparams mia.mcargs) in
-         applist (mia.mlf.(i-1),real_cargs)
-   | (DOPN(CoFix _,_)) as cofix ->
-       let cofix_def = contract_cofix cofix
-       in  mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
-   | _ -> assert false
-
+    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
+	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
+	let nparams    = mind_nparams env ind in
+	let real_cargs = snd (list_chop nparams mia.mcargs) in
+        applist (mia.mlf.(i-1),real_cargs)
+    | DOPN(CoFix _,_) as cofix ->
+	let cofix_def = contract_cofix cofix in
+	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
+    | _ -> assert false
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
 
@@ -541,208 +542,244 @@ let contract_fix = function
   | DOPN(Fix(recindices,bodynum),bodyvect) -> 
       let nbodies = Array.length recindices in
       let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
-    	sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
+      sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies)
   | _ -> assert false
 
-
 let fix_recarg fix stack =
   match fix with 
     | DOPN(Fix(recindices,bodynum),_) ->
     	if 0 <= bodynum & bodynum < Array.length recindices then
 	  let recargnum = Array.get recindices bodynum in
-            (try Some(recargnum, List.nth stack recargnum)
-             with Failure "nth" | Invalid_argument "List.nth" -> None)
+          (try Some(recargnum, List.nth stack recargnum)
+           with Failure "nth" | Invalid_argument "List.nth" -> None)
     	else None
     | _ -> assert false
 
-
 let reduce_fix whfun fix stack =
-    match fix with 
+  match fix with 
     | DOPN(Fix(recindices,bodynum),bodyvect) ->
     	(match fix_recarg fix stack with
-             None -> (false,(fix,stack))
+           | None -> (false,(fix,stack))
 	   | Some (recargnum,recarg) ->
                let (recarg'hd,_ as recarg') = whfun recarg [] in
                let stack' = list_assign stack recargnum (applist recarg') in
-		 (match recarg'hd with
-                      DOPN(MutConstruct _,_) -> 
-			(true,(contract_fix fix,stack'))
-		    | _ -> (false,(fix,stack'))))
+	       (match recarg'hd with
+                  | DOPN(MutConstruct _,_) -> 
+		      (true,(contract_fix fix,stack'))
+		  | _ -> (false,(fix,stack'))))
     | _ -> assert false
 
-(* NB : Cette fonction alloue pau c'est l'appel 
+(* NB : Cette fonction alloue peu c'est l'appel 
      ``let (recarg'hd,_ as recarg') = whfun recarg [] in''
                                      --------------------
 qui coute cher dans whd_betadeltaiota *)
 
-(**)
-
 let whd_betaiota_stack env = 
   let rec whrec x stack =
     match x with
-        DOP2(Cast,c,_) -> whrec c stack
+      | DOP2(Cast,c,_) -> whrec c stack
       | DOPN(AppL,cl)    -> whrec (array_hd cl) (array_app_tl cl stack)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with
-               [] -> (x,stack)
+             | [] -> (x,stack)
              | (a::m) -> stacklam whrec [a] c m)
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase x in
-          let (c,cargs) = whrec d []
-          in if reducible_mind_case c
-             then whrec (reduce_mind_case env
-                      {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
-             else (mkMutCaseA ci p (applist(c,cargs)) lf, stack)
-               
+          let (c,cargs) = whrec d [] in
+          if reducible_mind_case c then
+            whrec (reduce_mind_case env
+                     {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+          else 
+	    (mkMutCaseA ci p (applist(c,cargs)) lf, stack)
+            
       | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = reduce_fix whrec x stack
-          in if reduced then whrec fix stack
-             else (fix,stack)
-
+          let (reduced,(fix,stack)) = reduce_fix whrec x stack in
+          if reduced then whrec fix stack else (fix,stack)
       | x -> (x,stack)
-
-  in whrec    
-
+  in 
+  whrec    
 
 let whd_betaiota env x = applist (whd_betaiota_stack env x [])
 
 
 let whd_betadeltatiota_stack env = 
- let rec whrec x stack =
+  let rec whrec x stack =
     match x with
-        DOPN(Const _,_) ->
+      | DOPN(Const _,_) ->
           if translucent_const env x then
             whrec (const_value env x) stack
-          else (x,stack)
-
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
-          if translucent_abst env x then whrec (abst_value env x) stack
-          else (x,stack)
-
+          if translucent_abst env x then
+	    whrec (abst_value env x) stack
+          else
+	    (x,stack)
       | DOP2(Cast,c,_) -> whrec c stack
       | DOPN(AppL,cl)    -> whrec (array_hd cl) (array_app_tl cl stack)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with
-               [] -> (x,stack)
+             | [] -> (x,stack)
              | (a::m) -> stacklam whrec [a] c m)
-
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase x in
-          let (c,cargs) = whrec d []
-          in if reducible_mind_case c
-             then whrec (reduce_mind_case env
-                      {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
-             else (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
-
+          let (c,cargs) = whrec d [] in
+          if reducible_mind_case c then
+	    whrec (reduce_mind_case env
+                     {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+          else 
+	    (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
       | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = reduce_fix whrec x stack
-          in if reduced then whrec fix stack
-             else (fix,stack)
-
+          let (reduced,(fix,stack)) = reduce_fix whrec x stack in
+          if reduced then whrec fix stack else (fix,stack)
       | x -> (x,stack)
-
- in whrec   
-
+ in 
+  whrec   
 
 let whd_betadeltatiota env x = applist(whd_betadeltatiota_stack env x [])
 
-
 let whd_betadeltaiota_stack env =
   let rec bdi_rec x stack =
     match x with
-        DOPN(Const _,_) ->
-          if evaluable_const env x then bdi_rec (const_value env x) stack
-          else (x,stack)
-
+      | DOPN(Const _,_) ->
+          if evaluable_const env x then
+	    bdi_rec (const_value env x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
-          if evaluable_abst env x then bdi_rec (abst_value env x) stack else (x,stack)
-
+          if evaluable_abst env x then 
+	    bdi_rec (abst_value env x) stack 
+	  else 
+	    (x,stack)
       | DOP2(Cast,c,_) -> bdi_rec c stack
-
       | DOPN(AppL,cl) ->  bdi_rec (array_hd cl)  (array_app_tl cl stack)
-
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with
-               [] -> (x,stack)
+             | [] -> (x,stack)
              | (a::m) -> stacklam bdi_rec [a] c m)
-
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase x in
-          let (c,cargs) = bdi_rec d []
-          in if reducible_mind_case c
-             then bdi_rec (reduce_mind_case env
-                      {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
-             else (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
-
+          let (c,cargs) = bdi_rec d [] in
+          if reducible_mind_case c then
+            bdi_rec (reduce_mind_case env
+		       {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+          else 
+	    (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
       | DOPN(Fix _,_) -> 
-          let (reduced,(fix,stack)) = reduce_fix bdi_rec x stack
-          in if reduced then bdi_rec fix stack
-             else (fix,stack)
-
+          let (reduced,(fix,stack)) = reduce_fix bdi_rec x stack in
+          if reduced then bdi_rec fix stack else (fix,stack)
       | x -> (x,stack)
-
-  in bdi_rec
-
+  in
+  bdi_rec
 
 let whd_betadeltaiota env x = applist(whd_betadeltaiota_stack env x [])
-
-
+				
+				
 let whd_betadeltaiotaeta_stack env = 
   let rec whrec x stack =
     match x with
-        DOPN(Const _,_) ->
-          if evaluable_const env x then whrec (const_value env x) stack
-          else (x,stack)
+      | DOPN(Const _,_) ->
+          if evaluable_const env x then 
+	    whrec (const_value env x) stack
+          else 
+	    (x,stack)
       | DOPN(Abst _,_) ->
-          if evaluable_abst env x then whrec (abst_value env x) stack
-          else (x,stack)
-
+          if evaluable_abst env x then
+	    whrec (abst_value env x) stack
+          else 
+	    (x,stack)
       | DOP2(Cast,c,_) -> whrec c stack
-      | DOPN(AppL,cl)    -> whrec (array_hd cl) (array_app_tl cl stack)
+      | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with
-               [] ->
+             | [] ->
                  (match applist (whrec c []) with 
-                      (DOPN(AppL,cl)) -> 
+                    | DOPN(AppL,cl) -> 
                         (match whrec (array_last cl) [] with 
-                             (Rel 1,[]) ->
+                           | (Rel 1,[]) ->
                                let napp = (Array.length cl) -1 in
-                                 if napp = 0 then (x,stack) else
-                                   let lc = Array.sub cl 0 napp in
-                                   let u = if napp = 1 then lc.(0) else DOPN(AppL,lc) 
-                                   in if noccurn 1 u then (pop u,[]) else (x,stack)
+                               if napp = 0 then 
+				 (x,stack) 
+			       else
+                                 let lc = Array.sub cl 0 napp in
+                                 let u = 
+				   if napp = 1 then lc.(0) else DOPN(AppL,lc) 
+                                 in 
+				 if noccurn 1 u then (pop u,[]) else (x,stack)
                            | _ -> (x,stack))
                     | _ -> (x,stack))
              | (a::m) -> stacklam whrec [a] c m)
 
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase x in
-          let (c,cargs) = whrec d []
-          in if reducible_mind_case c
-             then whrec (reduce_mind_case env
-                      {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
-             else (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
-
+          let (c,cargs) = whrec d [] in
+          if reducible_mind_case c then
+	    whrec (reduce_mind_case env
+                     {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack
+          else 
+	    (mkMutCaseA ci p (applist(c,cargs)) lf,stack)
       | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = reduce_fix whrec x stack
-          in if reduced then whrec fix stack
-             else (fix,stack)
-
+          let (reduced,(fix,stack)) = reduce_fix whrec x stack in
+          if reduced then whrec fix stack else (fix,stack)
       | x -> (x,stack)
-
-  in whrec  
-
+  in 
+  whrec  
 
 let whd_betadeltaiotaeta env x = applist(whd_betadeltaiotaeta_stack env x [])
 
-
-
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
 
+type conversion_result =
+  | Convertible of universes
+  | NotConvertible
+
 type 'a conversion_function = 
-    'a unsafe_env -> constr -> constr -> bool * universes
+    'a unsafe_env -> constr -> constr -> conversion_result
+
+(* Conversion utility functions *)
+
+let convert_of_constraint f u =
+  match f u with
+    | Consistent u' -> Convertible u'
+    | Inconsistent -> NotConvertible
+
+let convert_of_bool b u =
+  if b then Convertible u else NotConvertible
+
+let bool_and_convert b f = 
+  if b then f else fun _ -> NotConvertible
+
+let convert_and f1 f2 u = 
+  match f1 u with
+    | Convertible u' -> f2 u'
+    | NotConvertible -> NotConvertible
+
+let convert_or f1 f2 u =
+  match f1 u with
+    | NotConvertible -> f2 u
+    | c -> c
+
+let forall2_conv f v1 v2 u =
+  array_fold_left2 
+    (fun a x y -> match a with
+       | NotConvertible -> NotConvertible
+       | Convertible u -> f x y u)
+    (Convertible u) v1 v2
+
+(* Convertibility of sorts *)
+
+let sort_cmp pb s0 s1 =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) -> convert_of_bool (c1 = c2)
+    | (Prop c1, Type u)  -> convert_of_bool (not (pb_is_equal pb))
+    | (Type u1, Type u2) ->
+	(match pb with
+           | CONV -> convert_of_constraint (enforce_eq u1 u2)
+	   | CONV_LEQ -> convert_of_constraint (enforce_geq u2 u1)
+	   | _ -> fun g -> Convertible g)
+    | (_, _) -> fun _ -> NotConvertible
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 
@@ -759,72 +796,86 @@ and eqappr cv_pb infos appr1 appr2 =
   match (frterm_of hd1, frterm_of hd2) with
     (* case of leaves *)
     | (FOP0(Sort s1), FOP0(Sort s2)) -> 
-        (Array.length v1 = 0) & (Array.length v2 = 0)
-	& sort_cmp (clos_infos_env infos) cv_pb s1 s2
+	bool_and_convert
+	  (Array.length v1 = 0 && Array.length v2 = 0)
+	  (sort_cmp cv_pb s1 s2)
 	  
     | (FVAR x1, FVAR x2) ->
-        (x1=x2)
-	& (array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+	bool_and_convert (x1=x2)
+	  (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
     | (FRel n, FRel m) ->
-        (reloc_rel n el1=reloc_rel m el2)
-        & (array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+        bool_and_convert 
+	  (reloc_rel n el1 = reloc_rel m el2)
+          (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
     | (FOP0(Meta(n)), FOP0(Meta(m))) ->
-        (n=m) 
-	& (array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+        bool_and_convert (n=m) 
+	  (forall2_conv (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
     | (FOP0 Implicit, FOP0 Implicit) ->
-        Array.length v1 = 0 & Array.length v2 = 0
+        convert_of_bool (Array.length v1 = 0 & Array.length v2 = 0)
 
     (* 2 constants or 2 abstractions *)
     | (FOPN(Const sp1,al1), FOPN(Const sp2,al2)) ->
-       uni_or_if (pb_is_univ_adjust cv_pb)
-       (fun () -> (* try first intensional equality *)
-           (sp1 == sp2 or sp1=sp2)
-         & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-         & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
-       (fun () -> (* else expand the second occurrence (arbitrary heuristic) *)
-           (match search_frozen_cst infos (Const sp2) al2 with
-              Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
-            | None -> (match search_frozen_cst infos (Const sp1) al1 with
-                        Some def1 -> eqappr cv_pb infos
-                            (lft1, fhnf_apply infos n1 def1 v1) appr2
-                      | None -> false)))
+	convert_or
+	  (* 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)))
+          (* else expand the second occurrence (arbitrary heuristic) *)
+          (match search_frozen_cst infos (Const sp2) al2 with
+             | Some def2 -> 
+		 eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
+             | None -> (match search_frozen_cst infos (Const sp1) al1 with
+                          | Some def1 -> eqappr cv_pb infos
+				(lft1, fhnf_apply infos n1 def1 v1) appr2
+			  | None -> fun _ -> NotConvertible))
+
     | (FOPN(Abst sp1,al1), FOPN(Abst sp2,al2)) ->
-       uni_or_if (pb_is_univ_adjust cv_pb)
-       (fun () -> (* try first intensional equality *)
-           sp1=sp2
-         & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-         & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
-       (fun () -> (* else expand the second occurrence (arbitrary heuristic) *)
+	convert_or
+	  (* 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)))
+          (* else expand the second occurrence (arbitrary heuristic) *)
           (match search_frozen_cst infos (Abst sp2) al2 with
-             Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
-           | None -> (match search_frozen_cst infos (Abst sp1) al2 with
-                        Some def1 -> eqappr cv_pb infos
-                            (lft1, fhnf_apply infos n1 def1 v1) appr2
-                      | None -> false)))
+             | Some def2 -> 
+		 eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
+             | None -> (match search_frozen_cst infos (Abst sp1) al2 with
+                          | Some def1 -> eqappr cv_pb infos
+				(lft1, fhnf_apply infos n1 def1 v1) appr2
+			  | None -> fun _ -> NotConvertible))
 
     (* only one constant or abstraction *)
     | (FOPN((Const _ | Abst _) as op,al1), _)      ->
         (match search_frozen_cst infos op al1 with
-           | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2
-           | None -> false)
+           | Some def1 -> 
+	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2
+           | None -> fun _ -> NotConvertible)
+
     | (_, FOPN((Const _ | Abst _) as op,al2))      ->
         (match search_frozen_cst infos op al2 with
-           | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
-           | None -> false)
+           | Some def2 -> 
+	       eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
+           | None -> fun _ -> NotConvertible)
 	
     (* other constructors *)
     | (FOP2(Lambda,c1,c2), FOP2(Lambda,c'1,c'2)) ->
-        (Array.length v1 = 0) & (Array.length v2 = 0)
-        & ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1
-        & ccnv (pb_equal cv_pb) infos el1 el2 c2 c'2
+        bool_and_convert
+	  (Array.length v1 = 0 && Array.length v2 = 0)
+          (convert_and
+	     (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1)
+             (ccnv (pb_equal cv_pb) infos el1 el2 c2 c'2))
 
     | (FOP2(Prod,c1,c2), FOP2(Prod,c'1,c'2)) ->
-        (Array.length v1 = 0) & (Array.length v2 = 0)
-        & ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1 (* Luo's system *)
-        & ccnv cv_pb infos el1 el2 c2 c'2
+	bool_and_convert
+          (Array.length v1 = 0 && Array.length v2 = 0)
+	  (convert_and
+             (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1) (* Luo's system *)
+             (ccnv cv_pb infos el1 el2 c2 c'2))
 
     (* Inductive types:  MutInd MutConstruct MutCase Fix Cofix *)
 
@@ -833,38 +884,43 @@ and eqappr cv_pb infos appr1 appr2 =
             sans que les annotations des MutCase le soient *)
 
     | (FOPN(MutCase _,cl1), FOPN(MutCase _,cl2)) ->
-        array_for_all2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2
-        & array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2
+        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)
 
      | (FOPN(op1,cl1), FOPN(op2,cl2)) ->
-         (op1 = op2)
-         & array_for_all2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2
-         & array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2
+	 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))
 
      (* binders *)
      | (FLAM(_,c1,_,_), FLAM(_,c2,_,_)) ->
-         (Array.length v1 = 0) & (Array.length v2 = 0)
-         & ccnv cv_pb infos (el_lift el1) (el_lift el2) c1 c2
+	 bool_and_convert
+           (Array.length v1 = 0 && Array.length v2 = 0)
+           (ccnv cv_pb infos (el_lift el1) (el_lift el2) c1 c2)
 
      | (FLAMV(_,vc1,_,_), FLAMV(_,vc2,_,_)) ->
-         (Array.length v1 = 0) & (Array.length v2 = 0)
-         & for_all2eq_vect (ccnv cv_pb infos (el_lift el1) (el_lift el2)) 
-	   vc1 vc2
+	 bool_and_convert
+           (Array.length v1 = 0 & Array.length v2 = 0)
+           (forall2_conv 
+	      (ccnv cv_pb infos (el_lift el1) (el_lift el2)) vc1 vc2)
 
-     | _ -> false
+     | _ -> (fun _ -> NotConvertible)
 
 
 let fconv cv_pb env t1 t2 =
-  let t1 = strong strip_outer_cast t1
-  and t2 = strong strip_outer_cast t2 in
+  let t1 = strong (fun _ -> strip_outer_cast) env t1
+  and t2 = strong (fun _ -> strip_outer_cast) env t2 in
+  let univ = universes env in
   if eq_constr t1 t2 then 
-    true
+    Convertible univ
   else
     let infos = create_clos_infos hnf_flags env in
-    ccnv cv_pb infos ELID ELID (inject t1) (inject t2)
+    ccnv cv_pb infos ELID ELID (inject t1) (inject t2) univ
 
-let conv       env term1 term2 = uni_pred (fconv CONV env term1) term2
-let conv_leq   env term1 term2 = uni_pred (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_x     env term1 term2 = fconv CONV_X env term1 term2
 let conv_x_leq env term1 term2 = fconv CONV_X_LEQ env term1 term2
 
@@ -873,31 +929,30 @@ let conv_x_leq env term1 term2 = fconv CONV_X_LEQ env term1 term2
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta mvmap = function
-    (DOP0(Meta p) as u) -> (try List.assoc p mvmap with Not_found -> u)
+let whd_meta env = function
+  | DOP0(Meta p) as u -> (try List.assoc p (metamap env) with Not_found -> u)
   | x -> x
-
-
+	
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
-let plain_instance s c = 
-  let rec irec u =
-    match u with
-        DOP0(Meta p)     -> (try List.assoc p s with Not_found -> u)
-      | DOP1(oper,c)     -> DOP1(oper, irec c)
-      | DOP2(oper,c1,c2) -> DOP2(oper, irec c1, irec c2)
-      | DOPN(oper,cl)    -> DOPN(oper, Array.map irec cl)
-      | DOPL(oper,cl)    -> DOPL(oper, List.map irec cl)
-      | DLAM(x,c)        -> DLAM(x, irec c)
-      | DLAMV(x,v)       -> DLAMV(x, Array.map irec v)
-      | _                -> u
-  in if s=[] then c else irec c
-
-
+let plain_instance env c = 
+  let s = metamap env in
+  let rec irec = function
+    | DOP0(Meta p) as u -> (try List.assoc p s with Not_found -> u)
+    | DOP1(oper,c)      -> DOP1(oper, irec c)
+    | DOP2(oper,c1,c2)  -> DOP2(oper, irec c1, irec c2)
+    | DOPN(oper,cl)     -> DOPN(oper, Array.map irec cl)
+    | DOPL(oper,cl)     -> DOPL(oper, List.map irec cl)
+    | DLAM(x,c)         -> DLAM(x, irec c)
+    | DLAMV(x,v)        -> DLAMV(x, Array.map irec v)
+    | u                 -> u
+  in 
+  if s = [] then c else irec c
+    
 (* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
-let instance s c = 
-    if s=[] then c else nf_betaiota (plain_instance s c)
-
+let instance env c = 
+  let s = metamap env in
+  if s = [] then c else nf_betaiota env (plain_instance env c)
 
 
 (* pseudo-reduction rule:
@@ -907,53 +962,49 @@ let instance s c =
  * error message.
  *)
 let hnf_prod_app env s t n =
-    match whd_betadeltaiota env t with
-    DOP2(Prod,_,b) -> sAPP b n
-  | _ ->
-    errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
-                      'sTR s ; 'fNL >]
-
+  match whd_betadeltaiota env t with
+    | DOP2(Prod,_,b) -> sAPP b n
+    | _ ->
+	errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
+			  'sTR s ; 'fNL >]
 
-let hnf_prod_appvect env s t nL = it_vect (hnf_prod_app env s) t nL
+let hnf_prod_appvect env s t nL = Array.fold_left (hnf_prod_app env s) t nL
 let hnf_prod_applist env s t nL = List.fold_left (hnf_prod_app env s) t nL
-
+				    
 let hnf_lam_app env s t n =
-    match whd_betadeltaiota env t with
-    DOP2(Lambda,_,b) -> sAPP b n
-  | _ ->
-    errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
-                      'sTR s ; 'fNL >]
+  match whd_betadeltaiota env t with
+    | DOP2(Lambda,_,b) -> sAPP b n
+    | _ ->
+	errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
+			  'sTR s ; 'fNL >]
 
-let hnf_lam_appvect env s t nL = it_vect (hnf_lam_app env s) t nL
+let hnf_lam_appvect env s t nL = Array.fold_left (hnf_lam_app env s) t nL
 let hnf_lam_applist env s t nL = List.fold_left (hnf_lam_app env s) t nL
 
 let splay_prod env = 
- let rec decrec m c =
-   match whd_betadeltaiota env c with
-     DOP2(Prod,a,DLAM(n,c_0))            -> decrec ((n,a)::m) c_0
-   | t -> m,t
- in decrec []
+  let rec decrec m c =
+    match whd_betadeltaiota env c with
+      | DOP2(Prod,a,DLAM(n,c_0))            -> decrec ((n,a)::m) c_0
+      | t -> m,t
+  in 
+  decrec []
   
-
-
 let decomp_prod env = 
- let rec decrec m c =
-   match whd_betadeltaiota env c with
-     (DOP0(Sort _) as x) -> m,x
-   | DOP2(Prod,a,DLAM(n,c_0))            -> decrec (m+1) c_0
-   | _                      -> error "decomp_prod: Not a product"
- in decrec 0
-  
-
+  let rec decrec m c =
+    match whd_betadeltaiota env c with
+      | DOP0(Sort _) as x -> m,x
+      | DOP2(Prod,a,DLAM(n,c_0))            -> decrec (m+1) c_0
+      | _                      -> error "decomp_prod: Not a product"
+  in 
+  decrec 0
+    
 let decomp_n_prod env n = 
- let rec decrec m ln c = if m = 0 then (ln,c) else 
-   match whd_betadeltaiota env c with
-     DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m-1) ((n,a)::ln) c_0
-   | _                      -> error "decomp_n_prod: Not enough products"
- in decrec n []
-  
-
-
+  let rec decrec m ln c = if m = 0 then (ln,c) else 
+    match whd_betadeltaiota env c with
+      | DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m-1) ((n,a)::ln) c_0
+      | _                      -> error "decomp_n_prod: Not enough products"
+  in 
+  decrec n []
 
 (* Special iota reduction... *)
 
@@ -962,43 +1013,44 @@ let contract_cofix_use_function f cofix =
     | DOPN(CoFix(bodynum),bodyvect) ->
   	let nbodies =  (Array.length bodyvect) -1 in
   	let make_Fi j = DOPN(CoFix(j),bodyvect) in
-  	let lbodies = list_assign (tabulate_list make_Fi nbodies) bodynum f 
-  	in  sAPPViList bodynum (last_vect bodyvect) lbodies
+  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+  	sAPPViList bodynum (array_last bodyvect) lbodies
     | _ -> assert false
 
-
-let reduce_mind_case_use_function f mia =
+let reduce_mind_case_use_function env f mia =
   match mia.mconstr with 
-     (DOPN(MutConstruct((indsp,tyindx),i),_)) ->
-       let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
-       let nparams    = mind_nparams ind in
-       let real_cargs = snd(chop_list nparams mia.mcargs)
-       in applist (mia.mlf.(i-1),real_cargs)
-   | (DOPN(CoFix _,_)) as cofix ->
-       let cofix_def = contract_cofix_use_function f cofix
-       in  mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
-   | _ -> assert false
-
-
+    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
+	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
+	let nparams    = mind_nparams env ind in
+	let real_cargs = snd(list_chop nparams mia.mcargs) in
+	applist (mia.mlf.(i-1),real_cargs)
+    | DOPN(CoFix _,_) as cofix ->
+	let cofix_def = contract_cofix_use_function f cofix in
+	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
+    | _ -> assert false
+	  
 let special_red_case env whfun p c ci lf  =
   let rec redrec c l = 
     let (constr,cargs) = whfun c l in 
-      match constr with 
-          (DOPN(Const _,_)) as g -> 
-            if (evaluable_const env g)
-            then
-              let gvalue = (const_value env g) 
-              in if reducible_mind_case  gvalue
-                 then reduce_mind_case_use_function g
-                   {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
-                 else redrec gvalue cargs
-            else raise Redelimination
-        | _ ->
-            if reducible_mind_case constr 
-            then reduce_mind_case
+    match constr with 
+      | DOPN(Const _,_) as g -> 
+          if (evaluable_const env g) then
+            let gvalue = (const_value env g) in
+            if reducible_mind_case  gvalue then
+              reduce_mind_case_use_function env g
+                {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
+            else 
+	      redrec gvalue cargs
+          else 
+	    raise Redelimination
+      | _ ->
+          if reducible_mind_case constr then
+            reduce_mind_case env
               {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf}
-            else raise Redelimination
-  in redrec c []
+          else 
+	    raise Redelimination
+  in 
+  redrec c []
 
 
 (* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make 
@@ -1009,25 +1061,24 @@ let contract_fix_use_function f fix =
     | DOPN(Fix(recindices,bodynum),bodyvect) ->
   	let nbodies = Array.length recindices in
   	let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
-  	let lbodies = list_assign (tabulate_list make_Fi nbodies) bodynum f in
-	  sAPPViList bodynum (last_vect bodyvect) lbodies
+  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+	  sAPPViList bodynum (array_last bodyvect) lbodies
     | _ -> assert false
 
 
 let reduce_fix_use_function f whfun fix stack =
-   match fix with 
-     |DOPN (Fix(recindices,bodynum),bodyvect) ->
-	 (match fix_recarg fix stack with
-              None -> (false,(fix,stack))
-	    | Some (recargnum,recarg) ->
-          	let (recarg'hd,_ as recarg')= whfun recarg [] in
-          	let stack' = list_assign stack recargnum (applist recarg') in
-		  (match recarg'hd with
-                       DOPN(MutConstruct _,_) ->
-			 (true,(contract_fix_use_function f fix,stack'))
-		     | _ -> (false,(fix,stack'))))
-     | _ -> assert false
-
+  match fix with 
+    | DOPN (Fix(recindices,bodynum),bodyvect) ->
+	(match fix_recarg fix stack with
+           | None -> (false,(fix,stack))
+	   | Some (recargnum,recarg) ->
+               let (recarg'hd,_ as recarg')= whfun recarg [] in
+               let stack' = list_assign stack recargnum (applist recarg') in
+	       (match recarg'hd with
+                  | DOPN(MutConstruct _,_) ->
+		      (true,(contract_fix_use_function f fix,stack'))
+		  | _ -> (false,(fix,stack'))))
+    | _ -> assert false
 
 
 (* Check that c is an "elimination constant"
@@ -1042,210 +1093,229 @@ an equivalent of Fix(f|t)[xi<-ai] as
 with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1]
    *)
 
-let compute_consteval c = 
+let compute_consteval env c = 
   let rec srec n labs c =
-    match whd_betadeltaeta_stack mt_evd c [] with 
-        (DOP2(Lambda,t,DLAM(_,g)),[])  -> srec (n+1) (t::labs) g
+    match whd_betadeltaeta_stack env c [] with 
+      | (DOP2(Lambda,t,DLAM(_,g)),[])  -> srec (n+1) (t::labs) g
       | (DOPN(Fix((nv,i)),bodies),l)   -> 
-          if (List.length l) > n then raise Elimconst 
+          if List.length l > n then 
+	    raise Elimconst 
           else
             let li = 
               List.map (function
-                            Rel k ->
-                              if for_all_vect (noccurn k) bodies 
-                              then (k, List.nth labs (k-1)) else raise Elimconst
-                          | _ -> raise Elimconst) l
-            in if (distinct (List.map fst li))  then (li,n,true) 
-               else raise Elimconst
+                          | Rel k ->
+                              if array_for_all (noccurn k) bodies then
+				(k, List.nth labs (k-1)) 
+			      else 
+				raise Elimconst
+                          | _ -> raise Elimconst) 
+		l
+            in 
+	    if (list_distinct (List.map fst li)) then 
+	      (li,n,true) 
+            else 
+	      raise Elimconst
       | (DOPN(MutCase _,_) as mc,lapp) -> 
-            (match destCase mc with
-                (_,_,Rel _,_) -> ([],n,false)
-              | _    -> raise Elimconst)
-      | _            -> raise Elimconst
+          (match destCase mc with
+             | (_,_,Rel _,_) -> ([],n,false)
+             | _    -> raise Elimconst)
+      | _ -> raise Elimconst
   in
-    try Some (srec 0 [] c)
-    with Elimconst -> None
-
+  try Some (srec 0 [] c) with Elimconst -> None
 
 let is_elim env c =
   let (sp, cl) = destConst c in
-    if (evaluable_const env c) 
-      & (defined_const env c) 
-      & (not((is_existential c))) 
-    then
-      let (_,cb) = const_of_path sp in 
-	((match cb.cONSTEVAL with
-              Some _ -> ()
-	    | None -> 
-		(match cb.cONSTBODY with
-		     Some{contents=COOKED b} ->
-		       cb.cONSTEVAL <- Some(compute_consteval b)
-		   | Some{contents=RECIPE _} ->
-		       anomalylabstrm "Reduction.is_elim"
-			 [< 'sTR"Found an uncooked transparent constant," ; 'sPC ;
-			    'sTR"which is supposed to be impossible" >]
-	 	   | _ -> assert false));
-         (match (cb.cONSTEVAL) with
-              Some (Some x) -> x
-	    | Some None -> raise Elimconst
-	    | _ -> assert false))
-    else raise Elimconst
-
+  if evaluable_const env c && defined_const env c && (not (is_existential c))
+  then
+    let (_,cb) = const_of_path env sp in 
+    begin match cb.const_eval with
+      | Some _ -> ()
+      | None -> 
+	  (match cb.const_body with
+	     | Some {contents = Cooked b} ->
+		 cb.const_eval <- Some (compute_consteval env b)
+	     | Some {contents = Recipe _} ->
+		 anomalylabstrm "Reduction.is_elim"
+		   [< 'sTR"Found an uncooked transparent constant," ; 'sPC ;
+		      'sTR"which is supposed to be impossible" >]
+	     | _ -> assert false)
+    end;
+    match (cb.const_eval) with
+      | Some (Some x) -> x
+      | Some None -> raise Elimconst
+      | _ -> assert false
+  else 
+    raise Elimconst
 
 (* takes the fn first elements of the list and gives them back lifted by ln 
    and in reverse order *)
 
 let rev_firstn_liftn fn ln = 
   let rec rfprec p res l = 
-    if p = 0 then res 
+    if p = 0 then 
+      res 
     else
       match l with
-          [] -> invalid_arg "Reduction.rev_firstn_liftn"
+        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
         | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
-  in rfprec fn [] 
+  in 
+  rfprec fn [] 
 
 let make_elim_fun env f largs =
-  try let (lv,n,b) = is_elim env f and ll = List.length largs
-      in if ll < n then raise Redelimination else
+  try 
+    let (lv,n,b) = is_elim env f 
+    and ll = List.length largs in
+    if ll < n then 
+      raise Redelimination 
+    else
       if b then
-      let labs,_ = chop_list n largs in
-      let p = List.length lv in
-        let la' = map_i (fun q aq ->
-                    try (Rel (p+1-(index (n+1-q) (List.map fst lv)))) 
-                    with Failure _ -> aq) 1
-                  (List.map (lift p) labs) in
-        it_list_i (fun i c (k,a) -> 
-                   DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
-                   DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv
-      else f
-  with Elimconst | Failure _ -> raise Redelimination
-
+	let labs,_ = list_chop n largs in
+	let p = List.length lv in
+        let la' = 
+	  list_map_i 
+	    (fun q aq ->
+	       try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) 
+	       with Failure _ -> aq) 
+	    1
+            (List.map (lift p) labs) 
+	in
+        list_fold_left_i 
+	  (fun i c (k,a) -> 
+             DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
+		  DLAM(Name(id_of_string"x"),c))) 
+	  0 (applistc f la') lv
+      else 
+	f
+  with 
+    | Elimconst | Failure _ -> raise Redelimination
 
 let rec red_elim_const env k largs =
   if not(evaluable_const env k) then raise Redelimination else
     let f = make_elim_fun env k largs in
-      match whd_betadeltaeta_stack env (const_value env k) largs with
-          (DOPN(MutCase _,_) as mc,lrest) ->
-            let (ci,p,c,lf) = destCase mc in
-            (special_red_case env (construct_const env) p c ci lf, lrest)
-
-        | (DOPN(Fix _,_) as fix,lrest) -> 
-            let (b,(c,rest)) = reduce_fix_use_function f (construct_const env) fix lrest
-            in if b then (nf_beta c, rest) else raise Redelimination
-
-        | _ -> assert false
+    match whd_betadeltaeta_stack env (const_value env k) largs with
+      | (DOPN(MutCase _,_) as mc,lrest) ->
+          let (ci,p,c,lf) = destCase mc in
+          (special_red_case env (construct_const env) p c ci lf, lrest)
+      | (DOPN(Fix _,_) as fix,lrest) -> 
+          let (b,(c,rest)) = 
+	    reduce_fix_use_function f (construct_const env) fix lrest
+          in 
+	  if b then (nf_beta env c, rest) else raise Redelimination
+      | _ -> assert false
 
 and construct_const env c stack = 
   let rec hnfstack x stack =
     match x with
-      (DOPN(Const _,_)) as k  ->
-        (try
-           let (c',lrest) = red_elim_const env k stack
-           in hnfstack c' lrest
-         with Redelimination ->
-           if evaluable_const env k 
-           then let cval = const_value env k
-           in  (match cval with
-                    DOPN (CoFix _,_) -> (k,stack)
-                  | _                -> hnfstack cval stack) 
-           else raise Redelimination)
-
-    | (DOPN(Abst _,_) as a) ->
-        if evaluable_abst a then hnfstack (abst_value a) stack
-        else raise Redelimination
-
-    | DOP2(Cast,c,_)   -> hnfstack c stack
-    | DOPN(AppL,cl)    -> hnfstack (hd_vect cl) (app_tl_vect cl stack)
-    | DOP2(Lambda,_,DLAM(_,c)) ->
-        (match stack with 
-             [] -> assert false
-           | c'::rest -> stacklam hnfstack [c'] c rest)
-    | DOPN(MutCase _,_) as c_0 ->
+      | (DOPN(Const _,_)) as k  ->
+          (try
+             let (c',lrest) = red_elim_const env k stack in
+             hnfstack c' lrest
+           with 
+	     | Redelimination ->
+		 if evaluable_const env k then
+		   let cval = const_value env k in
+		   (match cval with
+		      | DOPN (CoFix _,_) -> (k,stack)
+                      | _                -> hnfstack cval stack) 
+		 else 
+		   raise Redelimination)
+      | (DOPN(Abst _,_) as a) ->
+          if evaluable_abst env a then 
+	    hnfstack (abst_value env a) stack
+          else 
+	    raise Redelimination
+      | DOP2(Cast,c,_) -> hnfstack c stack
+      | DOPN(AppL,cl) -> hnfstack (array_hd cl) (array_app_tl cl stack)
+      | DOP2(Lambda,_,DLAM(_,c)) ->
+          (match stack with 
+             | [] -> assert false
+             | c'::rest -> stacklam hnfstack [c'] c rest)
+      | DOPN(MutCase _,_) as c_0 ->
           let (ci,p,c,lf) = destCase c_0 in
           hnfstack (special_red_case env (construct_const env) p c ci lf) stack
-    | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
-    | DOPN(CoFix _,_) as c_0 -> c_0,stack
-    | DOPN(Fix (_) ,_) as fix -> 
-        let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack
-        in if reduced then hnfstack fix stack' else raise Redelimination
-    | _ -> raise Redelimination
-  in hnfstack c stack
-
-
+      | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
+      | DOPN(CoFix _,_) as c_0 -> c_0,stack
+      | DOPN(Fix (_) ,_) as fix -> 
+          let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in
+          if reduced then hnfstack fix stack' else raise Redelimination
+      | _ -> raise Redelimination
+  in 
+  hnfstack c stack
 
 (* Hnf reduction tactic: *)
 let hnf_constr env c = 
   let rec redrec x largs =
     match x with
-        DOP2(Lambda,t,DLAM(n,c)) ->
+      | DOP2(Lambda,t,DLAM(n,c)) ->
           (match largs with
-               []      -> applist(x,largs)
+             | []      -> applist(x,largs)
              | a::rest -> stacklam redrec [a] c rest)
-      | DOPN(AppL,cl)   -> redrec (hd_vect cl) (app_tl_vect cl largs)
+      | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
       | DOPN(Const _,_) ->
           (try
-             let (c',lrest) = red_elim_const env x largs
-             in redrec c' lrest
+             let (c',lrest) = red_elim_const env x largs in
+             redrec c' lrest
            with Redelimination ->
-             if evaluable_const env x
-             then
-               let c = const_value env x
-               in match c with 
-                      DOPN(CoFix _,_) -> x
+             if evaluable_const env x then
+               let c = const_value env x in
+               match c with 
+                 | DOPN(CoFix _,_) -> x
                  | _ ->  redrec c largs
-             else applist(x,largs))
+             else 
+	       applist(x,largs))
       | DOPN(Abst _,_) ->
-          if evaluable_abst x then redrec (abst_value x) largs
-          else applist(x,largs)
-
+          if evaluable_abst env x then 
+	    redrec (abst_value env x) largs
+          else 
+	    applist(x,largs)
       | DOP2(Cast,c,_) -> redrec c largs
       | DOPN(MutCase _,_) ->
           let (ci,p,c,lf) = destCase x in
           (try
-             redrec (special_red_case env (whd_betadeltaiota_stack env) p c ci lf) largs
-           with Redelimination -> applist(x,largs))
+             redrec (special_red_case env (whd_betadeltaiota_stack env)
+		       p c ci lf) largs
+           with Redelimination -> 
+	     applist(x,largs))
       | (DOPN(Fix _,_)) ->
           let (reduced,(fix,stack)) = 
             reduce_fix (whd_betadeltaiota_stack env) x largs
-          in if reduced then redrec fix stack else applist(x,largs)
-
-      | _         -> applist(x,largs)
-
-  in redrec c []
+          in 
+	  if reduced then redrec fix stack else applist(x,largs)
+      | _ -> applist(x,largs)
+  in 
+  redrec c []
 
 
 (* Simpl reduction tactic: same as simplify, but also reduces elimination constants *)
 let whd_nf env c = 
   let rec nf_app c stack =
     match c with
-        DOP2(Lambda,c1,DLAM(name,c2))    ->
+      | DOP2(Lambda,c1,DLAM(name,c2))    ->
           (match stack with
-               [] -> (c,[])
+             | [] -> (c,[])
              | a1::rest -> stacklam nf_app [a1] c2 rest)
-
-      | DOPN(AppL,cl)      -> nf_app (hd_vect cl) (app_tl_vect cl stack)
+      | DOPN(AppL,cl)      -> nf_app (array_hd cl) (array_app_tl cl stack)
       | DOP2(Cast,c,_) -> nf_app c stack
       | DOPN(Const _,_) ->
           (try
-             let (c',lrest) = red_elim_const env c stack
-             in nf_app c' lrest
-           with Redelimination -> (c,stack))
+             let (c',lrest) = red_elim_const env c stack in
+             nf_app c' lrest
+           with Redelimination -> 
+	     (c,stack))
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase c in
           (try
              nf_app (special_red_case env nf_app p d ci lf) stack
-           with Redelimination -> (c,stack))
+           with Redelimination -> 
+	     (c,stack))
       | DOPN(Fix _,_) ->
-          let (reduced,(fix,rest)) = reduce_fix nf_app c stack
-          in if reduced then nf_app fix rest
-             else (fix,stack)
-
+          let (reduced,(fix,rest)) = reduce_fix nf_app c stack in
+          if reduced then nf_app fix rest else (fix,stack)
       | _ -> (c,stack)
+  in 
+  applist (nf_app c [])
 
-  in applist (nf_app c [])
-
-
-let nf env c = strong (whd_nf env) c
+let nf env c = strong (whd_nf env) env c
 
 
 (* Generic reduction: reduction functions used in reduction tactics *)
@@ -1260,7 +1330,6 @@ type red_expr =
   | Change of constr
   | Pattern of (int list * constr * constr) list
 
-
 let reduction_of_redexp = function
   | Red -> red_product
   | Hnf -> hnf_constr
@@ -1270,67 +1339,68 @@ let reduction_of_redexp = function
   | Unfold ubinds -> unfoldn ubinds
   | Fold cl -> fold_commands cl
   | Change t -> (fun _ _ -> t)
-  | Pattern lp -> (fun _ -> pattern_occs lp)
-
-
-
+  | Pattern lp -> pattern_occs lp
 
 (* Other reductions *)
 
 let one_step_reduce env = 
   let rec redrec largs x =
     match x with
-        DOP2(Lambda,t,DLAM(n,c))  ->
+      | DOP2(Lambda,t,DLAM(n,c))  ->
           (match largs with
-               []      -> error "Not reducible 1"
+             | []      -> error "Not reducible 1"
              | a::rest -> applistc (subst1 a c) rest)
-      | DOPN(AppL,cl) -> redrec (app_tl_vect cl largs) (hd_vect cl)
+      | DOPN(AppL,cl) -> redrec (array_app_tl cl largs) (array_hd cl)
       | DOPN(Const _,_) ->
           (try
-             let (c',l) = red_elim_const env x largs
-             in applistc c' l
+             let (c',l) = red_elim_const env x largs in
+             applistc c' l
            with Redelimination ->
-             if evaluable_const env x then
-               applistc (const_value env x) largs
-             else error "Not reductible 1")
+	     if evaluable_const env x then
+	       applistc (const_value env x) largs
+	     else 
+	       error "Not reductible 1")
       | DOPN(Abst _,_) ->
-          if evaluable_abst x then applistc (abst_value x) largs
-          else error "Not reducible 0"
-
+          if evaluable_abst env x then 
+	    applistc (abst_value env x) largs
+          else 
+	    error "Not reducible 0"
       | DOPN(MutCase _,_) ->
           let (ci,p,c,lf) = destCase x in
-          (try  applistc (special_red_case env (whd_betadeltaiota_stack env) p c ci lf) largs 
-           with Redelimination -> error "Not reducible 2")
+          (try  
+	     applistc (special_red_case env 
+			 (whd_betadeltaiota_stack env) p c ci lf) largs 
+           with Redelimination -> 
+	     error "Not reducible 2")
       | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = reduce_fix (whd_betadeltaiota_stack env) x largs
-          in if reduced then applistc fix stack else error "Not reducible 3"
-
-      | DOP2(Cast,c,_)   -> redrec largs c
-      | _              -> error "Not reducible 3"
-
-  in redrec []
-
+          let (reduced,(fix,stack)) = 
+	    reduce_fix (whd_betadeltaiota_stack env) x largs
+          in 
+	  if reduced then applistc fix stack else error "Not reducible 3"
+      | DOP2(Cast,c,_) -> redrec largs c
+      | _ -> error "Not reducible 3"
+  in 
+  redrec []
 
 (* One step of approximation *)
 
 let rec apprec env c stack =
-  let (t,stack) = whd_betaiota_stack c stack in
-    match t with
-      | DOPN(MutCase _,_) ->
-          let (ci,p,d,lf) = destCase t in
-          let (cr,crargs) = whd_betadeltaiota_stack env d [] in
-          let rslt = mkMutCaseA ci p (applist(cr,crargs)) lf in
-            if reducible_mind_case cr 
-            then apprec env rslt stack
-            else (t,stack)
-
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = reduce_fix (whd_betadeltaiota_stack env) t stack in
-            if reduced then apprec env fix stack
-            else (fix,stack)
-
-      | _ -> (t,stack)
-
+  let (t,stack) = whd_betaiota_stack env c stack in
+  match t with
+    | DOPN(MutCase _,_) ->
+        let (ci,p,d,lf) = destCase t in
+        let (cr,crargs) = whd_betadeltaiota_stack env d [] in
+        let rslt = mkMutCaseA ci p (applist(cr,crargs)) lf in
+        if reducible_mind_case cr then 
+	  apprec env rslt stack
+        else 
+	  (t,stack)
+    | DOPN(Fix _,_) ->
+        let (reduced,(fix,stack)) = 
+	  reduce_fix (whd_betadeltaiota_stack env) t stack 
+	in
+        if reduced then apprec env fix stack else (fix,stack)
+    | _ -> (t,stack)
 
 let hnf env c = apprec env c []
 
@@ -1341,41 +1411,38 @@ let hnf env c = apprec env c []
  * Used in Programs.
  * Added by JCF, 29/1/98. *)
 
-let whd_programs_stack = 
+let whd_programs_stack env = 
   let rec whrec x stack =
     match x with
-        DOPN(AppL,cl)    ->
+      | DOPN(AppL,cl)    ->
 	  if occur_meta cl.(1) then
 	    (x,stack)
 	  else
-	    whrec (hd_vect cl) (app_tl_vect cl stack)
+	    whrec (array_hd cl) (array_app_tl cl stack)
       | DOP2(Lambda,_,DLAM(_,c)) ->
           (match stack with
-               [] -> (x,stack)
+             | [] -> (x,stack)
              | (a::m) -> stacklam whrec [a] c m)
       | DOPN(MutCase _,_) ->
           let (ci,p,d,lf) = destCase x in
-	    if occur_meta d then
-	      (x,stack)
-	    else
-              let (c,cargs) = whrec d [] in
-              	if reducible_mind_case c then
-		  whrec (reduce_mind_case
-			   {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf})
+	  if occur_meta d then
+	    (x,stack)
+	  else
+            let (c,cargs) = whrec d [] in
+            if reducible_mind_case c then
+	      whrec (reduce_mind_case env
+		       {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf})
 		    stack
-		else
-		  (mkMutCaseA ci p (applist(c,cargs)) lf, stack)
-               
+	    else
+	      (mkMutCaseA ci p (applist(c,cargs)) lf, stack)
       | DOPN(Fix _,_) ->
           let (reduced,(fix,stack)) = reduce_fix whrec x stack in
           if reduced then whrec fix stack else (fix,stack)
-
       | x -> (x,stack)
+  in 
+  whrec    
 
-  in whrec    
-
-
-let whd_programs x = applist(whd_programs_stack x [])
+let whd_programs env x = applist (whd_programs_stack env x [])
 
 
 (* Used in several tactics, moved from tactics.ml *)
@@ -1387,171 +1454,166 @@ let whd_programs x = applist(whd_programs_stack x [])
 *)
 
 let reduce_to_mind env t = 
- let rec elimrec t l = 
-       match whd_castapp_stack t [] with
-           (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
-         | (DOPN(Const _,_),_) -> 
-             (try let t' = nf_betaiota (one_step_reduce env t)
-                  in elimrec t' l
-              with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
-                   [< 'sTR"Not an inductive product : it is a constant." >])
-         | (DOPN(MutCase _,_),_) ->
-             (try let t' = nf_betaiota (one_step_reduce env t)
-                      in elimrec t' l
-              with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
-              [< 'sTR"Not an inductive product: it is a case analysis term" >])
-         | (DOP2(Cast,c,_),[]) -> elimrec c l
-         | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
-         | _ -> error "Not an inductive product"
- in elimrec t []
+  let rec elimrec t l = 
+    match whd_castapp_stack t [] with
+      | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
+      | (DOPN(Const _,_),_) -> 
+          (try 
+	     let t' = nf_betaiota env (one_step_reduce env t) in
+             elimrec t' l
+           with UserError _ -> 
+	     errorlabstrm "tactics__reduce_to_mind"
+               [< 'sTR"Not an inductive product: it is a constant." >])
+      | (DOPN(MutCase _,_),_) ->
+          (try 
+	     let t' = nf_betaiota env (one_step_reduce env t) in
+             elimrec t' l
+           with UserError _ -> 
+	     errorlabstrm "tactics__reduce_to_mind"
+               [< 'sTR"Not an inductive product: it is a case analysis." >])
+      | (DOP2(Cast,c,_),[]) -> elimrec c l
+      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
+      | _ -> error "Not an inductive product"
+  in 
+  elimrec t []
     
-
 let reduce_to_ind env t =
- let (mind,redt,c) = reduce_to_mind env t
- in ((mind_path mind),redt,c)
-
-
+  let (mind,redt,c) = reduce_to_mind env t in
+  (mind_path mind, redt, c)
 
 let find_mrectype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
-    match t with
-        DOPN(MutInd (sp,i),_) ->  (t,l)
-      | _ -> raise Induc
-
+  match t with
+    | DOPN(MutInd (sp,i),_) ->  (t,l)
+    | _ -> raise Induc
 
 let find_minductype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
-    match t with
-        DOPN(MutInd (sp,i),_)
-          when mind_type_finite (snd (mind_of_path sp)) i -> (t,l)
-      | _ -> raise Induc
-
+  match t with
+    | DOPN(MutInd (sp,i),_)
+        when mind_type_finite (snd (mind_of_path sp)) i -> (t,l)
+    | _ -> raise Induc
 
 let find_mcoinductype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
-    match t with
-        DOPN(MutInd (sp,i),_)
-          when not (mind_type_finite (snd (mind_of_path sp)) i) -> (t,l)
-      | _ -> raise Induc
-
+  match t with
+    | DOPN(MutInd (sp,i),_)
+        when not (mind_type_finite (snd (mind_of_path sp)) i) -> (t,l)
+    | _ -> raise Induc
 
 let minductype_spec env c = 
-   try let (x,l) = find_minductype env c
-       in if l<>[] then anomaly "minductype_spec: Not a recursive type 1"
-          else x
-   with Induc -> anomaly "minductype_spec: Not a recursive type 2"
-
-
+  try 
+    let (x,l) = find_minductype env c in
+    if l<>[] then anomaly "minductype_spec: Not a recursive type 1" else x
+  with Induc -> 
+    anomaly "minductype_spec: Not a recursive type 2"
+      
 let mrectype_spec env c = 
-   try let (x,l) = find_mrectype env c
-       in if l<>[] then anomaly "mrectype_spec: Not a recursive type 1"
-          else x
-   with Induc -> anomaly "mrectype_spec: Not a recursive type 2"
-
+  try 
+    let (x,l) = find_mrectype env c in
+    if l<>[] then anomaly "mrectype_spec: Not a recursive type 1" else x
+  with Induc -> 
+    anomaly "mrectype_spec: Not a recursive type 2"
 
 let check_mrectype_spec env c =
-     try let (x,l) = find_mrectype env c
-         in if l<>[] then error "check_mrectype: Not a recursive type 1" else x
-     with Induc -> error "check_mrectype: Not a recursive type 2"
-
-
+  try 
+    let (x,l) = find_mrectype env c in
+    if l<>[] then error "check_mrectype: Not a recursive type 1" else x
+  with Induc -> 
+    error "check_mrectype: Not a recursive type 2"
 
 
 exception IsType
 
 let info_arity env = 
- let rec srec c = 
-  match whd_betadeltaiota env c with 
-      DOP0(Sort(Prop(Null)))  -> false 
-    | DOP0(Sort(Prop(Pos)))  -> true 
-    | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
-    | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
-    | _ -> raise IsType
- in srec 
-
+  let rec srec c = 
+    match whd_betadeltaiota env c with 
+      | DOP0(Sort(Prop(Null)))  -> false 
+      | DOP0(Sort(Prop(Pos)))  -> true 
+      | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
+      | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
+      | _ -> raise IsType
+  in 
+  srec 
+    
 let is_type_arity env = 
- let rec srec c = 
-  match whd_betadeltaiota env c with 
-      DOP0(Sort(Type(_)))  -> true
-    | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
-    | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
-    | _ -> false
- in srec 
-
-let is_logic_arity env c = try (not (info_arity env c))
-        with IsType -> false
-
-let is_info_arity env c = try (info_arity env c) 
-        with IsType -> true
+  let rec srec c = 
+    match whd_betadeltaiota env c with 
+      | DOP0(Sort(Type(_)))  -> true
+      | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
+      | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
+      | _ -> false
+  in 
+  srec 
+    
+let is_logic_arity env c = 
+  try (not (info_arity env c)) with IsType -> false
+
+let is_info_arity env c = 
+  try (info_arity env c) with IsType -> true
    
 let is_info_cast_type env c = 
-   match c with  DOP2(Cast,c,t) -> 
-                  (try info_arity env t 
-                   with IsType -> try info_arity env c with IsType -> true)
-               |  _ -> try info_arity env c with IsType -> true
-
+  match c with  
+    | DOP2(Cast,c,t) -> 
+	(try info_arity env t 
+         with IsType -> try info_arity env c with IsType -> true)
+    |  _ -> try info_arity env c with IsType -> true
+	   
 let contents_of_cast_type env c = 
-   if is_info_cast_type env c then Pos else Null
+  if is_info_cast_type env c then Pos else Null
 
-let is_info_sort = is_info_arity mt_evd
+let is_info_sort = is_info_arity
 
 (* calcul des arguments implicites *)
 
 (* la seconde liste est ordonne'e *)
 
 let ord_add x l =
-let rec aux l = match l with []    -> [x]
-                           | y::l' -> if y > x then x::l
-                                      else if x = y then l
-                                           else y::(aux l')
-in aux l
- 
-
+  let rec aux l = match l with 
+    | []    -> [x]
+    | y::l' -> if y > x then x::l else if x = y then l else y::(aux l')
+  in 
+  aux l
+    
 let add_free_rels_until depth m acc =
-let rec frec depth loc acc = function
-    Rel n         -> if (n <= depth) & (n > loc) then (ord_add (depth-n+1) acc) else acc
-  | DOPN(_,cl)    -> it_vect (frec depth loc) acc cl
-  | DOPL(_,cl)    -> List.fold_left (frec depth loc) acc cl
-  | DOP2(_,c1,c2) -> frec depth loc (frec depth loc acc c1) c2
-  | DOP1(_,c)     -> frec depth loc acc c
-  | DLAM(_,c)     -> frec (depth+1) (loc+1) acc c
-  | DLAMV(_,cl)   -> it_vect (frec (depth+1) (loc+1)) acc cl
-  | VAR _         -> acc
-  | DOP0 _        -> acc
-in frec depth 0 acc m 
-
+  let rec frec depth loc acc = function
+    | Rel n -> 
+	if (n <= depth) & (n > loc) then (ord_add (depth-n+1) acc) else acc
+    | DOPN(_,cl)    -> Array.fold_left (frec depth loc) acc cl
+    | DOPL(_,cl)    -> List.fold_left (frec depth loc) acc cl
+    | DOP2(_,c1,c2) -> frec depth loc (frec depth loc acc c1) c2
+    | DOP1(_,c)     -> frec depth loc acc c
+    | DLAM(_,c)     -> frec (depth+1) (loc+1) acc c
+    | DLAMV(_,cl)   -> Array.fold_left (frec (depth+1) (loc+1)) acc cl
+    | VAR _         -> acc
+    | DOP0 _        -> acc
+  in 
+  frec depth 0 acc m 
 
 (* calcule la liste des arguments implicites *)
 
-let poly_args t =
- let rec aux n t = match (whd_betadeltaiota mt_evd t) with
-    (DOP2(Prod,a,DLAM(_,b))) -> add_free_rels_until n a (aux (n+1) b)
-  | (DOP2(Cast,t',_)) -> aux n t'
-  | _ -> []
-
-in match (strip_outer_cast (whd_betadeltaiota mt_evd t)) 
-    with (DOP2(Prod,a,DLAM(_,b))) -> aux 1 b
-        | _ -> []
-
-
+let poly_args env t =
+  let rec aux n t = match (whd_betadeltaiota env t) with
+    | DOP2(Prod,a,DLAM(_,b)) -> add_free_rels_until n a (aux (n+1) b)
+    | DOP2(Cast,t',_) -> aux n t'
+    | _ -> []
+  in 
+  match (strip_outer_cast (whd_betadeltaiota env t)) with 
+    | DOP2(Prod,a,DLAM(_,b)) -> aux 1 b
+    | _ -> []
 
 (* Expanding existential variables (trad.ml, progmach.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
 let rec whd_ise env = function
-    (DOPN(Const sp,_) as k) ->
-      if Evd.in_dom env sp then
+  | DOPN(Const sp,_) as k ->
+      if Evd.in_dom (evar_map env) sp then
         if defined_const env k then
           whd_ise env (const_value env k)
         else
-(*
-          let pk = Printer.prterm k in
-          let pkt = Printer.prterm (const_type env k) in
-            errorlabstrm "whd_ise"
-              [< 'sTR"Undefined evar "; pk; 'sTR" : "; pkt >]
-*)
-            errorlabstrm "whd_ise"
-              [< 'sTR"There is an unknown subterm I cannot solve" >]
-      else k
+          errorlabstrm "whd_ise"
+            [< 'sTR"There is an unknown subterm I cannot solve" >]
+      else 
+	k
   | DOP2(Cast,c,_) -> whd_ise env c
   | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ)))
   | c -> c
@@ -1559,34 +1621,33 @@ let rec whd_ise env = function
 
 (* 2- undefined existentials are left unchanged *)
 let rec whd_ise1 env = function
-    (DOPN(Const sp,_) as k) ->
-    if Evd.in_dom env sp & defined_const env k then
+  | (DOPN(Const sp,_) as k) ->
+      if Evd.in_dom (evar_map env) sp & defined_const env k then
         whd_ise1 env (const_value env k)
-    else k
+      else 
+	k
   | DOP2(Cast,c,_) -> whd_ise1 env c
   | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ)))
   | c -> c
 
-
-let nf_ise1 env = strong (whd_ise1 env)
+let nf_ise1 env = strong (whd_ise1 env) env
 
 (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
  * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
 
 let rec whd_ise1_metas env = function
-    (DOPN(Const sp,_) as k) ->
-    if Evd.in_dom env sp then
-      if defined_const env k then
-      	whd_ise1_metas env (const_value env k)
-      else 
-      	let m = DOP0(Meta (newMETA())) in
+  | (DOPN(Const sp,_) as k) ->
+      if Evd.in_dom (evar_map env) sp then
+	if defined_const env k then
+      	  whd_ise1_metas env (const_value env k)
+	else 
+      	  let m = DOP0(Meta (new_meta())) in
 	  DOP2(Cast,m,const_type env k)
-    else
-      k
+      else
+	k
   | DOP2(Cast,c,_) -> whd_ise1_metas env c
   | c -> c
 
-
 (* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
 
 let under_outer_cast f = function
@@ -1597,21 +1658,21 @@ let rec strip_all_casts t =
   match t with
     | DOP2 (Cast, b, _) -> strip_all_casts b
     | DOP0 _ as t -> t
-	(* Cas ad hoc *)
+    (* Cas ad hoc *)
     | DOPN(Fix _ as f,v) -> 
 	let n = Array.length v in
 	let ts = Array.sub v 0 (n-1) in
 	let b = v.(n-1) in 
-	  DOPN(f, Array.append 
-		 (Array.map strip_all_casts ts)
-		 [|under_outer_cast strip_all_casts b|])
+	DOPN(f, Array.append 
+	       (Array.map strip_all_casts ts)
+	       [|under_outer_cast strip_all_casts b|])
     | DOPN(CoFix _ as f,v) -> 
 	let n = Array.length v in
 	let ts = Array.sub v 0 (n-1) in
 	let b = v.(n-1) in 
-	  DOPN(f, Array.append 
-		 (Array.map strip_all_casts ts)
-		 [|under_outer_cast strip_all_casts b|])
+	DOPN(f, Array.append 
+	       (Array.map strip_all_casts ts)
+	       [|under_outer_cast strip_all_casts b|])
     | DOP1(oper,c) -> DOP1(oper,strip_all_casts c)
     | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2)
     | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index f8646c9027..058db0a117 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -33,57 +33,57 @@ val stack_reduction_of_reduction :
 (* Generic Optimized Reduction Functions using Closures *)
 
 (* 1. lazy strategy *)
-val clos_norm_flags : Closure.flags -> 'c unsafe_env -> 'a reduction_function
+val clos_norm_flags : Closure.flags -> 'a reduction_function
 (* Same as (strong whd_beta[delta][iota]), but much faster on big terms *) 
 val nf_beta : 'a reduction_function
 val nf_betaiota : 'a reduction_function
-val nf_betadeltaiota : 'c unsafe_env -> 'a reduction_function
+val nf_betadeltaiota : 'a reduction_function
 
 (* 2. call by value strategy *)
-val cbv_norm_flags : flags -> 'c unsafe_env -> 'a reduction_function
+val cbv_norm_flags : flags -> 'a reduction_function
 val cbv_beta : 'a reduction_function
 val cbv_betaiota : 'a reduction_function
-val cbv_betadeltaiota : 'c unsafe_env -> 'a reduction_function
+val cbv_betadeltaiota : 'a reduction_function
 
 (* 3. lazy strategy, weak head reduction *)
 val whd_beta : 'a reduction_function
 val whd_betaiota : 'a reduction_function
-val whd_betadeltaiota : 'c unsafe_env -> 'a reduction_function
+val whd_betadeltaiota : 'a reduction_function
 
 val whd_beta_stack : 'a stack_reduction_function
 val whd_betaiota_stack : 'a stack_reduction_function
-val whd_betadeltaiota_stack : 'c unsafe_env -> 'a stack_reduction_function
+val whd_betadeltaiota_stack : 'a stack_reduction_function
 
 
 (* Head normal forms *)
-val whd_const_stack : section_path list -> 'c unsafe_env -> 'a stack_reduction_function
-val whd_const : section_path list -> 'c unsafe_env -> 'a reduction_function
-val whd_delta_stack : 'c unsafe_env -> 'a stack_reduction_function
-val whd_delta : 'c unsafe_env -> 'a reduction_function
-val whd_betadelta_stack : 'c unsafe_env -> 'a stack_reduction_function
-val whd_betadelta : 'c unsafe_env -> 'a reduction_function
-val whd_betadeltat_stack : 'c unsafe_env -> 'a stack_reduction_function
-val whd_betadeltat : 'c unsafe_env -> 'a reduction_function
-val whd_betadeltatiota_stack : 'c unsafe_env -> 'a stack_reduction_function
-val whd_betadeltatiota : 'c unsafe_env -> 'a reduction_function
-val whd_betadeltaiotaeta_stack : 'c unsafe_env -> 'a stack_reduction_function
-val whd_betadeltaiotaeta : 'c unsafe_env -> 'a reduction_function
+val whd_const_stack : section_path list -> 'a stack_reduction_function
+val whd_const : section_path list -> 'a reduction_function
+val whd_delta_stack : 'a stack_reduction_function
+val whd_delta : 'a reduction_function
+val whd_betadelta_stack : 'a stack_reduction_function
+val whd_betadelta : 'a reduction_function
+val whd_betadeltat_stack : 'a stack_reduction_function
+val whd_betadeltat : 'a reduction_function
+val whd_betadeltatiota_stack : 'a stack_reduction_function
+val whd_betadeltatiota : 'a reduction_function
+val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
+val whd_betadeltaiotaeta : 'a reduction_function
 
 val beta_applist : (constr * constr list) -> constr
 
 
 (* Special-Purpose Reduction Functions *)
-val whd_meta : (int * constr) list -> 'a reduction_function
-val plain_instance : (int * constr) list -> 'a reduction_function
-val instance : (int * constr) list -> 'a reduction_function
+val whd_meta : 'a reduction_function
+val plain_instance : 'a reduction_function
+val instance : 'a reduction_function
 
-val whd_ise : 'a unsafe_env -> 'a reduction_function
-val whd_ise1 : 'a unsafe_env -> 'a reduction_function
-val nf_ise1 : 'a unsafe_env -> 'a reduction_function
-val whd_ise1_metas : 'a unsafe_env -> 'a reduction_function
+val whd_ise : 'a reduction_function
+val whd_ise1 : 'a reduction_function
+val nf_ise1 : 'a reduction_function
+val whd_ise1_metas : 'a reduction_function
 
-val red_elim_const : 'c unsafe_env -> 'a stack_reduction_function
-val one_step_reduce : 'c unsafe_env -> constr -> constr
+val red_elim_const : 'a stack_reduction_function
+val one_step_reduce : 'a reduction_function
 
 val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
@@ -98,12 +98,12 @@ val decomp_n_prod :
   'c unsafe_env -> int -> constr -> ((name * constr) list) * constr
 
 val is_info_arity : 'c unsafe_env -> constr -> bool
-val is_info_sort : constr -> bool
+val is_info_sort : 'c unsafe_env -> constr -> bool
 val is_logic_arity : 'c unsafe_env -> constr -> bool
 val is_type_arity : 'c unsafe_env -> constr -> bool
 val is_info_cast_type : 'c unsafe_env -> constr -> bool
 val contents_of_cast_type : 'c unsafe_env -> constr -> contents
-val poly_args : constr -> int list
+val poly_args : 'a unsafe_env -> constr -> int list
 val reduce_to_mind : 'c unsafe_env -> constr -> constr * constr * constr
 val reduce_to_ind  : 'c unsafe_env -> constr -> 
                                 section_path*constr*constr
@@ -122,24 +122,28 @@ type red_expr =
   | Change of constr
   | Pattern of (int list * constr * constr) list
 
-
-val nf : 'c unsafe_env -> 'a reduction_function
+val nf : 'a reduction_function
 val unfoldn : 
-  (int list * section_path) list -> 'c unsafe_env -> 'a reduction_function
-val fold_one_com : 'c unsafe_env -> constr -> 'a reduction_function
-val fold_commands : constr list -> 'c unsafe_env -> 'a reduction_function
+  (int list * section_path) list -> 'a reduction_function
+val fold_one_com : constr -> 'a reduction_function
+val fold_commands : constr list -> 'a reduction_function
 val subst_term_occ : int list -> constr -> constr -> constr
-val pattern_occs : (int list * constr * constr) list -> constr -> constr
-val hnf_constr : 'c unsafe_env -> constr -> constr
-val compute : 'c unsafe_env -> 'a reduction_function
-val reduction_of_redexp : red_expr -> 'c unsafe_env -> constr -> constr
-
+val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
+val hnf_constr : 'a reduction_function
+val compute : 'a reduction_function
+val reduction_of_redexp : red_expr -> 'a reduction_function
 
 
 (* Conversion Functions (uses closures, lazy strategy) *)
 
+type conversion_result =
+  | Convertible of universes
+  | NotConvertible
+
 type 'a conversion_function = 
-    'a unsafe_env -> constr -> constr -> bool * universes
+    '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/univ.mli b/kernel/univ.mli
index 3916296724..392b9544f5 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,3 +12,17 @@ val prop_univ_univ : universe
 val prop_univ_univ_univ : universe
 
 type universes
+
+val initial_universes : universes
+
+type constraint_result = 
+  | Consistent of universes
+  | Inconsistent
+
+type constraint_function = 
+    universe -> universe -> universes -> constraint_result
+
+val enforce_gt : constraint_function
+val enforce_geq : constraint_function
+val enforce_eq : constraint_function
+