Nouvelle version de frterm; ajout des contextes dans l'enviornnement de réduction de Closure

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

4 files changed, 680 insertions, 631 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 783017e8a4..0bb893c6f7 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -16,48 +16,98 @@ let share = ref true
 (* Profiling *)
 let beta = ref 0
 let delta = ref 0
+let letin = ref 0
+let evar = ref 0
 let iota = ref 0
 let prune = ref 0
 
 let reset () =
-  beta := 0; delta := 0; iota := 0; prune := 0
+  beta := 0; delta := 0; letin := 0; evar := 0; iota := 0; prune := 0
 
 let stop() =
   mSGNL [< 'sTR"[Reds: beta=";'iNT !beta; 'sTR" delta="; 'iNT !delta;
+	   'sTR" letin="; 'iNT !letin; 'sTR" evar="; 'iNT !evar;
            'sTR" iota="; 'iNT !iota; 'sTR" prune="; 'iNT !prune; 'sTR"]" >]
 
 
-(* sets of reduction kinds *)
-type red_kind = BETA | DELTA of sorts oper | IOTA
-
-(* Hack: we use oper (Const "$LOCAL VAR$") for local variables *)
-let local_const_oper = Const (make_path [] (id_of_string "$LOCAL VAR$") CCI)
-
+(* [r_const=(true,cl)] means all constants but those in [cl] *)
+(* [r_const=(false,cl)] means only those in [cl] *)
 type reds = {
   r_beta : bool;
-  r_delta : sorts oper -> bool; (* this is unsafe: exceptions may pop out *)
+  r_const : bool * section_path list;
+  r_letin : bool;
+  r_evar : bool;
   r_iota : bool }
 
 let betadeltaiota_red = {
   r_beta = true;
-  r_delta = (fun _ -> true);
+  r_const = true,[];
+  r_letin = true;
+  r_evar = true;
   r_iota = true } 
 
 let betaiota_red = {
   r_beta = true;
-  r_delta = (fun _ -> false);
+  r_const = false,[];
+  r_letin = false;
+  r_evar = false;
   r_iota = true }
 		     
 let beta_red = {
   r_beta = true;
-  r_delta = (fun _ -> false);
+  r_const = false,[];
+  r_letin = false;
+  r_evar = false;
   r_iota = false }
 
 let no_red = {
   r_beta = false;
-  r_delta = (fun _ -> false);
+  r_const = false,[];
+  r_letin = false;
+  r_evar = false;
   r_iota = false }
 
+let betaiotaletin_red = {
+  r_beta = true;
+  r_const = false,[];
+  r_letin = true;
+  r_evar = false;
+  r_iota = true }
+
+let unfold_red sp = {
+  r_beta = true;
+  r_const = false,[sp];
+  r_letin = false;
+  r_evar = false;
+  r_iota = true }
+
+(* Sets of reduction kinds.
+   Main rule: delta implies all consts (both global (= by
+   section_path) and local (= by Rel or Var)), all evars, and letin's.
+   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
+   a LetIn expression is Letin reduction *)
+
+type red_kind =
+    BETA | DELTA | LETIN | EVAR | IOTA
+  | CONST of section_path list | CONSTBUT of section_path list
+
+let rec red_add red = function
+  | BETA -> { red with r_beta = true }
+  | DELTA ->
+      if snd red.r_const <> [] then error "Conflict in the reduction flags";
+      { red with r_const = true,[]; r_letin = true; r_evar = true }
+  | CONST cl ->
+      if fst red.r_const then error "Conflict in the reduction flags";
+      { red with r_const = false, list_union cl (snd red.r_const) }
+  | CONSTBUT cl ->
+      if not (fst red.r_const) & snd red.r_const <> [] then
+	error "Conflict in the reduction flags";
+      { red with r_const = true, list_union cl (snd red.r_const);
+	  r_letin = true; r_evar = true }
+  | IOTA -> { red with r_iota = true }
+  | EVAR -> { red with r_evar = true }
+  | LETIN -> { red with r_letin = true }
+
 let incr_cnt red cnt =
   if red then begin
     if !stats then incr cnt;
@@ -65,11 +115,21 @@ let incr_cnt red cnt =
   end else 
     false
 
+let red_local_const red = fst red.r_const
+
+(* to know if a redex is allowed, only a subset of red_kind is used ... *)
 let red_set red = function
   | BETA -> incr_cnt red.r_beta beta
-  | DELTA op -> incr_cnt (red.r_delta op) delta
+  | CONST [sp] -> 
+      let (b,l) = red.r_const in
+      let c = List.mem sp l in
+      incr_cnt ((b & not c) or (c & not b)) delta
+  | LETIN -> incr_cnt red.r_letin letin
+  | EVAR -> incr_cnt red.r_letin evar
   | IOTA -> incr_cnt red.r_iota iota
-
+  | DELTA -> fst red.r_const  (* Used for Rel/Var defined in context *)
+  (* Not for internal use *)
+  | CONST _ | CONSTBUT _ -> failwith "not implemented"
 
 (* specification of the reduction function *)
 
@@ -89,7 +149,8 @@ let beta = (UNIFORM,beta_red)
 let betaiota = (UNIFORM,betaiota_red)
 let betadeltaiota = (UNIFORM,betadeltaiota_red)
 
-let hnf_flags = (SIMPL,betaiota_red)
+let hnf_flags = (SIMPL,betaiotaletin_red)
+let unfold_flags sp = (UNIFORM, unfold_red sp)
 
 let flags_under = function
   | (SIMPL,r) -> (WITHBACK,r)
@@ -114,54 +175,9 @@ let red_under (md,r) rk =
     | WITHBACK -> true
     | _ -> red_set r rk
 
-
-(* Flags of reduction and cache of constants: 'a is a type that may be
- * mapped to constr. 'a infos implements a cache for constants and
- * abstractions, storing a representation (of type 'a) of the body of
- * this constant or abstraction.
- *  * i_evc is the set of constraints for existential variables
- *  * i_tab is the cache table of the results
- *  * i_repr is the function to get the representation from the current
- *         state of the cache and the body of the constant. The result
- *         is stored in the table.
- *
- * const_value_cache searchs in the tab, otherwise uses i_repr to
- * compute the result and store it in the table. If the constant can't
- * be unfolded, returns None, but does not store this failure.  * This
- * doesn't take the RESET into account. You mustn't keep such a table
- * after a Reset.  * This type is not exported. Only its two
- * instantiations (cbv or lazy) are.
- *)
-
-type ('a, 'b) infos = {
-  i_flags : flags;
-  i_repr : ('a, 'b) infos -> constr -> 'a;
-  i_env : env;
-  i_evc : 'b evar_map;
-  i_tab : (constr, 'a) Hashtbl.t }
-
-let const_value_cache info c =
-  try  
-    Some (Hashtbl.find info.i_tab c)
-  with Not_found ->
-    match const_evar_opt_value info.i_env info.i_evc c with
-      | Some body ->
-          let v = info.i_repr info body in
-          Hashtbl.add info.i_tab c v;
-          Some v
-      | None -> None
-
-let infos_under infos =
-  { i_flags = flags_under infos.i_flags; 
-    i_repr = infos.i_repr; 
-    i_env = infos.i_env; 
-    i_evc = infos.i_evc;
-    i_tab = infos.i_tab }
-
-
-(* explicit substitutions of type 'a *)
+(* (bounded) explicit substitutions of type 'a *)
 type 'a subs =
-  | ESID                   (* ESID       =          identity *)
+  | ESID of int            (* ESID(n)    = %n END   bounded identity *)
   | CONS of 'a * 'a subs   (* CONS(t,S)  = (S.t)    parallel substitution *)
   | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
                            (*                        with n vars *)
@@ -174,8 +190,7 @@ type 'a subs =
 let subs_cons(x,s) = CONS(x,s)
 
 let subs_liftn n = function
-  | ESID -> ESID         (* the identity lifted is still the identity *)
-                         (* (because (^1.1) --> id) *)
+  | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *)
   | LIFT (p,lenv) -> LIFT (p+n, lenv)
   | lenv -> LIFT (n,lenv)
 
@@ -197,26 +212,113 @@ let subs_shft = function
  *    [(%n S)] k  --> k         if k <= n
  *    [(%n S)] k  --> [^n]([S](k-n))
  *
- * the result is (Inr k) when the variable is just relocated
+ * the result is (Inr (k+lams,p)) when the variable is just relocated
+ * where p is None if the variable points insider subs and Some(k) if the
+ * variable points k bindings beyond subs.
  *) 
 let rec exp_rel lams k subs =
   match (k,subs) with
     | (1, CONS (def,_)) -> Inl(lams,def)
     | (_, CONS (_,l)) -> exp_rel lams (pred k) l
-    | (_, LIFT (n,_)) when k<=n -> Inr(lams+k)
+    | (_, LIFT (n,_)) when k<=n -> Inr(lams+k,None)
     | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l
     | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s
-    | (_, ESID) -> Inr(lams+k)
-
+    | (_, ESID n) when k<=n -> Inr(lams+k,None)
+    | (_, ESID n) -> Inr(lams+k,None)
+(* TO DEBUG
+    | (_, ESID n) -> Inr(lams+k,Some (k-n))
+*)
 let expand_rel k subs = exp_rel 0 k subs
 
+(* Flags of reduction and cache of constants: 'a is a type that may be
+ * mapped to constr. 'a infos implements a cache for constants and
+ * abstractions, storing a representation (of type 'a) of the body of
+ * this constant or abstraction.
+ *  * i_evc is the set of constraints for existential variables
+ *  * i_tab is the cache table of the results
+ *  * i_repr is the function to get the representation from the current
+ *         state of the cache and the body of the constant. The result
+ *         is stored in the table.
+ *
+ * ref_value_cache searchs in the tab, otherwise uses i_repr to
+ * compute the result and store it in the table. If the constant can't
+ * be unfolded, returns None, but does not store this failure.  * This
+ * doesn't take the RESET into account. You mustn't keep such a table
+ * after a Reset.  * This type is not exported. Only its two
+ * instantiations (cbv or lazy) are.
+ *)
+
+type table_key =
+  | ConstBinding of constant
+  | EvarBinding of existential
+  | VarBinding of identifier
+  | FarRelBinding of int
+
+type ('a, 'b) infos = {
+  i_flags : flags;
+  i_repr : ('a, 'b) infos -> int -> constr -> 'a;
+  i_env : env;
+  i_evc : 'b evar_map;
+  i_rels : int * (int * constr) list;
+  i_vars : (identifier * constr) list;
+  i_tab : (table_key, 'a) Hashtbl.t }
+
+let ref_value_cache info ref =
+  try  
+    Some (Hashtbl.find info.i_tab ref)
+  with Not_found ->
+  try
+    let n, body =
+      match ref with
+	| FarRelBinding n -> let (s,l) = info.i_rels in (n, List.assoc (s-n) l)
+	| VarBinding id -> 0, List.assoc id info.i_vars
+	| EvarBinding evc -> 0, existential_value info.i_evc evc
+	| ConstBinding cst -> 0, constant_value info.i_env cst
+    in
+    let v = info.i_repr info n body in
+    Hashtbl.add info.i_tab ref v;
+    Some v
+  with
+    | Not_found (* List.assoc *)
+    | NotInstantiatedEvar (* Evar *)
+    | NotEvaluableConst _ (* Const *)
+      -> None
+
+let make_constr_ref n = function
+  | FarRelBinding _ -> mkRel n
+  | VarBinding id -> mkVar id
+  | EvarBinding evc -> mkEvar evc
+  | ConstBinding cst -> mkConst cst
+
+let defined_vars flags env =
+  if red_local_const (snd flags) then
+    fold_var_context 
+      (fun env (id,b,t) e ->
+	 match b with
+	   | None -> e
+	   | Some body -> (id, body)::e)
+      env []
+  else []
+
+let defined_rels flags env =
+  if red_local_const (snd flags) then
+  fold_rel_context 
+      (fun env (id,b,t) (i,subs) ->
+	 match b with
+	   | None -> (i+1, subs)
+	   | Some body -> (i+1, (i,body) :: subs))
+      env (0,[])
+  else (0,[])
+
+let infos_under infos = { infos with i_flags = flags_under infos.i_flags }
+
 
 (**** Call by value reduction ****)
 
 (* The type of terms with closure. The meaning of the constructors and
  * the invariants of this datatype are the following:
  *  VAL(k,c) represents the constr c with a delayed shift of k. c must be
- *          in normal form and neutral (i.e. not a lambda, a constr or a
+ *          in normal form and neutral (i.e. not a lambda, a construct or a
  *          (co)fix, because they may produce redexes by applying them,
  *          or putting them in a case)
  *  LAM(x,a,b,S) is the term [S]([x:a]b). the substitution is propagated
@@ -328,6 +430,10 @@ let red_allowed flags stack rk =
   else 
     red_top flags rk
 
+let red_allowed_ref flags stack = function
+  | FarRelBinding _ | VarBinding _ -> red_allowed flags stack DELTA
+  | EvarBinding _ -> red_allowed flags stack EVAR
+  | ConstBinding (sp,_) -> red_allowed flags stack (CONST [sp])
 
 (* Transfer application lists from a value to the stack
  * useful because fixpoints may be totally applied in several times
@@ -340,7 +446,7 @@ let strip_appl head stack =
     | _ -> (head, stack)
 
 
-(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
+(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, its last
  * argument is [].
  * Because we must put all the applied terms in the stack.
  *)
@@ -405,20 +511,27 @@ let rec norm_head info env t stack =
    * when reducing closed terms, n is always 0 *)
   | IsRel i -> (match expand_rel i env with
                 | Inl (0,v) ->
-                    reduce_const_body (cbv_norm_more info) v stack
+                    reduce_const_body (cbv_norm_more info env) v stack
                 | Inl (n,v) ->
                     reduce_const_body
-                      (cbv_norm_more info) (shift_value n v) stack
-                | Inr n -> (VAL(0, Rel n), stack))
+                      (cbv_norm_more info env) (shift_value n v) stack
+                | Inr (n,None) ->
+		    (VAL(0, mkRel n), stack)
+                | Inr (n,Some p) ->
+		    norm_head_ref n info env stack (FarRelBinding p))
+
+  | IsVar id -> norm_head_ref 0 info env stack (VarBinding id)
+
   | IsConst (sp,vars) ->
-      let normt = mkConst (sp,Array.map (cbv_norm_term info env) vars) in
-      if red_allowed info.i_flags stack (DELTA (Const sp)) then
-	match const_value_cache info normt with
-          | Some body -> reduce_const_body (cbv_norm_more info) body stack
-          | None -> (VAL(0,normt), stack)
-      else (VAL(0,normt), stack)
+      let normt = (sp,Array.map (cbv_norm_term info env) vars) in
+      norm_head_ref 0 info env stack (ConstBinding normt)
+
+  | IsEvar (n,vars) -> 
+      let normt = (n,Array.map (cbv_norm_term info env) vars) in
+      norm_head_ref 0 info env stack (EvarBinding normt)
+
   | IsLetIn (x, b, t, c) ->
-      if red_allowed info.i_flags stack (DELTA local_const_oper) then
+      if red_allowed info.i_flags stack LETIN then
 	let b = cbv_stack_term info TOP env b in 
         norm_head info (subs_cons (b,env)) c stack
       else
@@ -427,13 +540,6 @@ let rec norm_head info env t stack =
 		   cbv_norm_term info env t,
 		   cbv_norm_term info (subs_lift env) c) in
 	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
-  | IsEvar (n,vars) -> 
-      let normt = mkEvar (n,Array.map (cbv_norm_term info env) vars) in
-      if red_allowed info.i_flags stack (DELTA (Evar n)) then
-	match const_value_cache info normt with
-          | Some body -> reduce_const_body (cbv_norm_more info) body stack
-          | None -> (VAL(0,normt), stack)
-      else (VAL(0,normt), stack)
 
   (* non-neutral cases *)
   | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack)
@@ -443,7 +549,7 @@ let rec norm_head info env t stack =
       (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack)
 
   (* neutral cases *)
-  | (IsVar _ | IsSort _ | IsMeta _ | IsXtra _ ) -> (VAL(0, t), stack)
+  | (IsSort _ | IsMeta _ | IsXtra _ ) -> (VAL(0, t), stack)
   | IsMutInd (sp,vars) -> 
       (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack)
   | IsProd (x,t,c) -> 
@@ -451,6 +557,14 @@ let rec norm_head info env t stack =
 		      cbv_norm_term info (subs_lift env) c)),
 	     stack)
 
+and norm_head_ref k info env stack normt =
+  if red_allowed_ref info.i_flags stack normt then
+    match ref_value_cache info normt with
+      | Some body ->
+	  reduce_const_body (cbv_norm_more info env) (shift_value k body) stack
+      | None -> (VAL(0,make_constr_ref k normt), stack)
+  else (VAL(0,make_constr_ref k normt), stack)
+
 (* cbv_stack_term performs weak reduction on constr t under the subs
  * env, with context stack, i.e. ([env]t stack).  First computes weak
  * head normal form of t and checks if a redex appears with the stack.
@@ -467,13 +581,13 @@ and cbv_stack_term info stack env t =
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,_), stk)
-        when fixp_reducible (cbv_norm_more info) info.i_flags fix stk ->
+        when fixp_reducible (cbv_norm_more info env) info.i_flags fix stk ->
         let (envf,redfix) = contract_fixp env fix in
         cbv_stack_term info stk envf redfix
 
     (* constructor guard satisfied or Cofix in a Case -> IOTA *)
     | (COFIXP(cofix,env,_), stk)
-        when cofixp_reducible (cbv_norm_more info) info.i_flags cofix stk ->
+        when cofixp_reducible (cbv_norm_more info env) info.i_flags cofix stk->
         let (envf,redfix) = contract_cofixp env cofix in
         cbv_stack_term info stk envf redfix
 
@@ -501,10 +615,10 @@ and cbv_stack_term info stack env t =
 
 
 (* if we are in SIMPL mode, maybe v isn't reduced enough *)
-and cbv_norm_more info v =
+and cbv_norm_more info env v =
   match (v, info.i_flags) with
     | (VAL(k,t), ((SIMPL|WITHBACK),_)) ->
-        cbv_stack_term (infos_under info) TOP (subs_shft (k,ESID)) t
+        cbv_stack_term (infos_under info) TOP (subs_shft (k,env)) t
     | _ -> v
 
 
@@ -558,21 +672,25 @@ type 'a cbv_infos = (cbv_value, 'a) infos
 (* constant bodies are normalized at the first expansion *)
 let create_cbv_infos flgs env sigma =
   { i_flags = flgs;
-    i_repr = (fun old_info c -> cbv_stack_term old_info TOP ESID c);
+    i_repr = (fun old_info n c -> cbv_stack_term old_info TOP (ESID (-n)) c);
     i_env = env;
     i_evc = sigma;
+    i_rels = defined_rels flgs env;
+    i_vars = defined_vars flgs env;
     i_tab = Hashtbl.create 17 }
 
 
 (* with profiling *)
 let cbv_norm infos constr =
+  let repr_fun = cbv_stack_term infos TOP in
   if !stats then begin
     reset();
-    let r= cbv_norm_term infos ESID constr in
+    let r= cbv_norm_term infos (ESID 0) constr in
     stop();
     r
   end else
-    cbv_norm_term infos ESID constr
+    cbv_norm_term infos (ESID 0) constr
+
 
 (**** End of call by value ****)
 
@@ -593,25 +711,28 @@ type freeze = {
 
 and frterm =
   | FRel of int
-  | FVAR of identifier
-  | FOP0 of sorts oper
-  | FOP1 of sorts oper * freeze
-  | FOP2 of sorts oper * freeze * freeze
-  | FOPN of sorts oper * freeze array
-  | FLAM of name * freeze * constr * freeze subs
-  | FLAMV of name * freeze array * constr array * freeze subs
-  | FLam of name * type_freeze * freeze * constr * freeze subs
-  | FPrd of name * type_freeze * freeze * constr * freeze subs
-  | FLet of name * freeze * type_freeze * freeze * constr * freeze subs
+  | FAtom of constr
+  | FCast of freeze * freeze
+  | FFlex of frreference * freeze array
+  | FInd of inductive_path * freeze array
+  | FConstruct of constructor_path * freeze array
+  | FApp of freeze * freeze array
+  | FFix of (int array * int) * (freeze array * name list * freeze array)
+      * constr array * freeze subs
+  | FCoFix of int * (freeze array * name list * freeze array)
+      * constr array * freeze subs
+  | FCases of case_info * freeze * freeze * freeze array
+  | FLambda of name * freeze * freeze * constr * freeze subs
+  | FProd of name * freeze * freeze * constr * freeze subs
+  | FLetIn of name * freeze * freeze * freeze * constr * freeze subs
   | FLIFT of int * freeze
   | FFROZEN of constr * freeze subs
 
-(* Cas où typed_type est casté en interne
-and type_freeze = freeze * sorts
- *)
-(* Cas où typed_type n'est pas casté *)
-and type_freeze = freeze
-(**)
+and frreference =
+  | FConst of section_path
+  | FEvar of existential_key
+  | FVar of identifier
+  | FFarRel of int * int
 
 (*
 let typed_map f t = f (body_of_type t), level_of_type t
@@ -650,7 +771,7 @@ let freeze_assign v1 v2 =
 let rec lift_frterm n v =
   match v.term with
     | FLIFT (k,f) -> lift_frterm (k+n) f
-    | (FOP0 _ | FVAR _) as ft -> { norm = true; term = ft }
+    | FAtom _ as ft -> { norm = true; term = ft }
      	(* gene: closed terms *)
     | _ -> { norm = v.norm; term = FLIFT (n,v) }
 
@@ -661,7 +782,7 @@ let rec lift_frterm n v =
  * notations above). *)
 let lift_freeze n v =
   match (n, v.term) with
-    | (0, _) | (_, (FOP0 _ | FVAR _)) -> v   (* identity lift or closed term *)
+    | (0, _) | (_, FAtom _ ) -> v  (* identity lift or closed term *)
     | _ -> lift_frterm n v
 
 
@@ -669,69 +790,116 @@ let freeze env t = { norm = false; term = FFROZEN (t,env) }
 let freeze_vect env v = Array.map (freeze env) v
 let freeze_list env l = List.map (freeze env) l
 
+let freeze_rec env (tys,lna,bds) =
+  let env' = subs_liftn (Array.length bds) env in
+  (Array.map (freeze env) tys, lna, Array.map (freeze env') bds)
+
+
 (* pourrait peut-etre remplacer freeze ?! (et alors FFROZEN
  * deviendrait inutile) *)
 
 let rec traverse_term env t =
-  match t with
-    | Rel i -> (match expand_rel i env with
+  match kind_of_term t with
+    | IsRel i -> (match expand_rel i env with
 		  | Inl (lams,v) -> (lift_frterm lams v)
-		  | Inr k -> { norm = true; term = FRel k })
-    | VAR x -> { norm = true; term = FVAR x }
-    | DOP0 op ->  { norm = true; term = FOP0 op }
-    | DOP1 (op, nt) -> { norm = false; term = FOP1 (op, traverse_term env nt) }
-    | DOP2 (op,a,b) ->
+		  | Inr (k,None) -> { norm = true; term = FRel k }
+		  | Inr (k,Some p) ->
+		      { norm = false; term = FFlex (FFarRel (k,p), [||]) })
+    | IsVar x -> { norm = false; term = FFlex (FVar x, [||]) }
+    | IsMeta _ | IsSort _ | IsXtra _ ->  { norm = true; term = FAtom t }
+    | IsCast (a,b) ->
         { norm = false;
-          term = FOP2 (op, traverse_term env a, traverse_term env b)}
-    | DOPN (op,v) ->
-        { norm = false; term = FOPN (op, Array.map (traverse_term env) v) }
-    | DLAM (x,a) ->
+          term = FCast (traverse_term env a, traverse_term env b)}
+    | IsAppL (f,v) ->
         { norm = false;
-          term = FLAM (x, traverse_term (subs_lift env) a, a, env) }
-    | DLAMV (x,ve) ->
-        { norm = (ve=[||]);
-          term = FLAMV (x, Array.map (traverse_term (subs_lift env)) ve,
-                        ve, env) }
-    | CLam (n,t,c) ->
+	  term = FApp (traverse_term env f, Array.map (traverse_term env) v) }
+    | IsMutInd (sp,v) ->
+        { norm = false; term = FInd (sp, Array.map (traverse_term env) v) }
+    | IsMutConstruct (sp,v) ->
+        { norm = false; term = FConstruct (sp,Array.map (traverse_term env) v)}
+    | IsConst (sp,v) ->
         { norm = false;
-	  term = FLam (n, traverse_type env t, traverse_term (subs_lift env) c,
-		       c, env) }
-    | CPrd (n,t,c)   ->
+	  term = FFlex (FConst sp, Array.map (traverse_term env) v) }
+    | IsEvar (sp,v) ->
         { norm = false;
-	  term = FPrd (n, traverse_type env t, traverse_term (subs_lift env) c,
-		       c, env) }
-    | CLet (n,b,t,c) ->
+	  term = FFlex (FEvar sp, Array.map (traverse_term env) v) }
+
+    | IsMutCase (ci,p,c,v) ->
         { norm = false;
-	  term = FLet (n, traverse_term env b, traverse_type env t,
-		       traverse_term (subs_lift env) c,
-		       c, env) }
+	  term = FCases (ci, traverse_term env p, traverse_term env c,
+			 Array.map (traverse_term env) v) }
+    | IsFix (op,(tys,lna,bds)) ->
+	let env' = subs_liftn (Array.length bds) env in
+        { norm = false;
+	  term = FFix (op, (Array.map (traverse_term env) tys, lna,
+			    Array.map (traverse_term env') bds),
+		       bds, env) }
+    | IsCoFix (op,(tys,lna,bds)) ->
+	let env' = subs_liftn (Array.length bds) env in
+        { norm = false;
+	  term = FCoFix (op, (Array.map (traverse_term env) tys, lna,
+			      Array.map (traverse_term env') bds),
+			 bds, env) }
 
-and traverse_type env = typed_map (traverse_term env)
+    | IsLambda (n,t,c) ->
+        { norm = false;
+	  term = FLambda (n, traverse_term env t,
+			  traverse_term (subs_lift env) c,
+			  c, env) }
+    | IsProd (n,t,c)   ->
+        { norm = false;
+	  term = FProd (n, traverse_term env t, 
+			traverse_term (subs_lift env) c,
+			c, env) }
+    | IsLetIn (n,b,t,c) ->
+        { norm = false;
+	  term = FLetIn (n, traverse_term env b, traverse_term env t,
+			 traverse_term (subs_lift env) c,
+			 c, env) }
 
 (* Back to regular terms: remove all FFROZEN, keep casts (since this
  * fun is not dedicated to the Calculus of Constructions). 
  *)
 let rec lift_term_of_freeze lfts v =
   match v.term with
-    | FRel i -> Rel (reloc_rel i lfts)
-    | FVAR x -> VAR x
-    | FOP0 op -> DOP0 op
-    | FOP1 (op,a) -> DOP1 (op, lift_term_of_freeze lfts a)
-    | FOP2 (op,a,b) ->
-        DOP2 (op, lift_term_of_freeze lfts a, lift_term_of_freeze lfts b)
-    | FOPN (op,ve) -> DOPN (op, Array.map (lift_term_of_freeze lfts) ve)
-    | FLAM (x,a,_,_) -> DLAM (x, lift_term_of_freeze (el_lift lfts) a)
-    | FLAMV (x,ve,_,_) ->
-        DLAMV (x, Array.map (lift_term_of_freeze (el_lift lfts)) ve)
-    | FLam (n,t,c,_,_)   ->
-	CLam (n, typed_unmap (lift_term_of_freeze lfts) t, 
-	      lift_term_of_freeze (el_lift lfts) c)
-    | FPrd (n,t,c,_,_)   ->
-	CPrd (n, typed_unmap (lift_term_of_freeze lfts) t, 
+    | FRel i -> mkRel (reloc_rel i lfts)
+    | FFlex (FVar x, v) -> assert (v=[||]); mkVar x
+    | FFlex (FFarRel (i,p), v) -> assert (v=[||]); mkRel (reloc_rel i lfts)
+    | FAtom c -> c
+    | FCast (a,b) ->
+        mkCast (lift_term_of_freeze lfts a, lift_term_of_freeze lfts b)
+    | FFlex (FConst op,ve) ->
+	mkConst (op, Array.map (lift_term_of_freeze lfts) ve)
+    | FFlex (FEvar op,ve) ->
+	mkEvar (op, Array.map (lift_term_of_freeze lfts) ve)
+    | FInd (op,ve) ->
+	mkMutInd (op, Array.map (lift_term_of_freeze lfts) ve)
+    | FConstruct (op,ve) -> 
+	mkMutConstruct (op, Array.map (lift_term_of_freeze lfts) ve)
+    | FCases (ci,p,c,ve) ->
+	mkMutCase (ci, lift_term_of_freeze lfts p,
+		   lift_term_of_freeze lfts c,
+		   Array.map (lift_term_of_freeze lfts) ve)
+    | FFix (op,(tys,lna,bds),_,_) ->
+	let lfts' = el_liftn (Array.length bds) lfts in
+	mkFix (op, (Array.map (lift_term_of_freeze lfts) tys, lna,
+		    Array.map (lift_term_of_freeze lfts') bds))
+    | FCoFix (op,(tys,lna,bds),_,_) ->
+	let lfts' = el_liftn (Array.length bds) lfts in
+	mkCoFix (op, (Array.map (lift_term_of_freeze lfts) tys, lna,
+		      Array.map (lift_term_of_freeze lfts') bds))
+    | FApp (f,ve) ->
+	mkAppL (lift_term_of_freeze lfts f,
+		Array.map (lift_term_of_freeze lfts) ve)
+    | FLambda (n,t,c,_,_)   ->
+	mkLambda (n, lift_term_of_freeze lfts t, 
 	      lift_term_of_freeze (el_lift lfts) c)
-    | FLet (n,b,t,c,_,_) ->
-	CLet (n, lift_term_of_freeze lfts b,
-	      typed_unmap (lift_term_of_freeze lfts) t,
+    | FProd (n,t,c,_,_)   ->
+	mkProd (n, lift_term_of_freeze lfts t, 
+		lift_term_of_freeze (el_lift lfts) c)
+    | FLetIn (n,b,t,c,_,_) ->
+	mkLetIn (n, lift_term_of_freeze lfts b,
+	      lift_term_of_freeze lfts t,
 	      lift_term_of_freeze (el_lift lfts) c)
     | FLIFT (k,a) -> lift_term_of_freeze (el_shft k lfts) a
     | FFROZEN (t,env) ->
@@ -750,25 +918,44 @@ let applist_of_freeze appl = Array.to_list (Array.map term_of_freeze appl)
  *)
 let rec fstrong unfreeze_fun lfts v =
   match (unfreeze_fun v).term with
-    | FRel i -> Rel (reloc_rel i lfts)
-    | FVAR x -> VAR x
-    | FOP0 op -> DOP0 op
-    | FOP1 (op,a) -> DOP1 (op, fstrong unfreeze_fun lfts a)
-    | FOP2 (op,a,b) ->
-        DOP2 (op, fstrong unfreeze_fun lfts a, fstrong unfreeze_fun lfts b)
-    | FOPN (op,ve) -> DOPN (op, Array.map (fstrong unfreeze_fun lfts) ve)
-    | FLAM (x,a,_,_) -> DLAM (x, fstrong unfreeze_fun (el_lift lfts) a)
-    | FLAMV (x,ve,_,_) ->
-        DLAMV (x, Array.map (fstrong unfreeze_fun (el_lift lfts)) ve)
-    | FLam (n,t,c,_,_)   ->
-	CLam (n, typed_unmap (fstrong unfreeze_fun lfts) t,
+    | FRel i -> mkRel (reloc_rel i lfts)
+    | FFlex (FFarRel (i,p), v) -> assert (v=[||]); mkRel (reloc_rel i lfts)
+    | FFlex (FVar x, v) -> assert (v=[||]); mkVar x
+    | FAtom c -> c
+    | FCast (a,b) ->
+        mkCast (fstrong unfreeze_fun lfts a, fstrong unfreeze_fun lfts b)
+    | FFlex (FConst op,ve) ->
+	mkConst (op, Array.map (fstrong unfreeze_fun lfts) ve)
+    | FFlex (FEvar op,ve) ->
+	mkEvar (op, Array.map (fstrong unfreeze_fun lfts) ve)
+    | FInd (op,ve) ->
+	mkMutInd (op, Array.map (fstrong unfreeze_fun lfts) ve)
+    | FConstruct (op,ve) -> 
+	mkMutConstruct (op, Array.map (fstrong unfreeze_fun lfts) ve)
+    | FCases (ci,p,c,ve) ->
+	mkMutCase (ci, fstrong unfreeze_fun lfts p,
+		   fstrong unfreeze_fun lfts c,
+		   Array.map (fstrong unfreeze_fun lfts) ve)
+    | FFix (op,(tys,lna,bds),_,_) ->
+	let lfts' = el_liftn (Array.length bds) lfts in
+	mkFix (op, (Array.map (fstrong unfreeze_fun lfts) tys, lna,
+		    Array.map (fstrong unfreeze_fun lfts') bds))
+    | FCoFix (op,(tys,lna,bds),_,_) ->
+	let lfts' = el_liftn (Array.length bds) lfts in
+	mkCoFix (op, (Array.map (fstrong unfreeze_fun lfts) tys, lna,
+		      Array.map (fstrong unfreeze_fun lfts') bds))
+    | FApp (f,ve) ->
+	mkAppL (fstrong unfreeze_fun lfts f,
+		Array.map (fstrong unfreeze_fun lfts) ve)
+    | FLambda (n,t,c,_,_)   ->
+	mkLambda (n, fstrong unfreeze_fun lfts t,
 	      fstrong unfreeze_fun (el_lift lfts) c)
-    | FPrd (n,t,c,_,_)   ->
-	CPrd (n, typed_unmap (fstrong unfreeze_fun lfts) t,
+    | FProd (n,t,c,_,_)   ->
+	mkProd (n, fstrong unfreeze_fun lfts t,
 	      fstrong unfreeze_fun (el_lift lfts) c)
-    | FLet (n,b,t,c,_,_) ->
-	CLet (n, fstrong unfreeze_fun lfts b,
-	      typed_unmap (fstrong unfreeze_fun lfts) t,
+    | FLetIn (n,b,t,c,_,_) ->
+	mkLetIn (n, fstrong unfreeze_fun lfts b,
+	      fstrong unfreeze_fun lfts t,
 	      fstrong unfreeze_fun (el_lift lfts) c)
     | FLIFT (k,a) -> fstrong unfreeze_fun (el_shft k lfts) a
     | FFROZEN _ -> anomaly "Closure.fstrong"
@@ -776,7 +963,7 @@ let rec fstrong unfreeze_fun lfts v =
 
 (* Build a freeze, which represents the substitution of arg in t
  * Used to constract a beta-redex:
- *           [^depth](FLam(S,t)) arg -> [(^depth o S).arg]t
+ *           [^depth](FLamda(S,t)) arg -> [(^depth o S).arg]t
  *)
 let rec contract_subst depth t subs arg =
   freeze (subs_cons (arg, subs_shft (depth,subs))) t
@@ -786,16 +973,13 @@ let rec contract_subst depth t subs arg =
 
 type fconstr = freeze
 
-let inject constr = freeze ESID constr
-
 (* Remove head lifts, applications and casts *)
 let rec strip_frterm n v stack =
   match v.term with
     | FLIFT (k,f) -> strip_frterm (k+n) f stack
-    | FOPN (AppL,appl) ->
-        strip_frterm n appl.(0)
-          ((Array.map (lift_freeze n) (array_tl appl))::stack)
-    | FOP2 (Cast,f,_) -> (strip_frterm n f stack)
+    | FApp (f,args) ->
+        strip_frterm n f ((Array.map (lift_freeze n) args)::stack)
+    | FCast (f,_) -> (strip_frterm n f stack)
     | _ -> (n, v, Array.concat stack)
 
 let strip_freeze v = strip_frterm 0 v []
@@ -803,52 +987,49 @@ let strip_freeze v = strip_frterm 0 v []
 
 (* Same as contract_fixp, but producing a freeze *)
 (* does not deal with FLIFT *)
-let contract_fix_vect unf_fun fix =
-  let (bnum, bodies, make_body) =
+let contract_fix_vect fix =
+  let (thisbody, make_body, env, nfix) =
     match fix with
-      | FOPN(Fix(reci,i),bvect) ->
-          (i, array_last bvect,
-           (fun j -> { norm = false; term = FOPN(Fix(reci,j), bvect) }))
-      | FOPN(CoFix i,bvect) ->
-          (i, array_last bvect,
-           (fun j -> { norm = false; term = FOPN(CoFix j, bvect) }))
+      | FFix ((reci,i),def,bds,env) ->
+          (bds.(i),
+	   (fun j -> { norm = false; term = FFix ((reci,j),def,bds,env) }),
+	   env, Array.length bds)
+      | FCoFix (i,def,bds,env) ->
+          (bds.(i),
+	   (fun j -> { norm = false; term = FCoFix (j,def,bds,env) }),
+	   env, Array.length bds)
       | _ -> anomaly "Closure.contract_fix_vect: not a (co)fixpoint" 
   in
-  let rec subst_bodies_from_i i depth bds =
-    let ubds = unf_fun bds in
-    match ubds.term with
-      | FLAM(_,_,t,env) ->
-          subst_bodies_from_i (i+1) depth
-            (freeze (subs_cons (make_body i, env)) t)
-      | FLAMV(_,_,tv,env) ->
-          freeze (subs_shft (depth, subs_cons (make_body i, env))) tv.(bnum)
-      | FLIFT(k,lbds) -> subst_bodies_from_i i (k+depth) lbds
-      | _ -> anomaly "Closure.contract_fix_vect: malformed (co)fixpoint"
+  let rec subst_bodies_from_i i env =
+    if i = nfix then
+      freeze env thisbody
+    else
+      subst_bodies_from_i (i+1) (subs_cons (make_body i, env))
   in       
-  subst_bodies_from_i 0 0 bodies
+  subst_bodies_from_i 0 env
 
 
 (* CoFix reductions are context dependent. Therefore, they cannot be shared. *)
-let copy_case ci cl ft =
-  let ncl = Array.copy cl in
-  ncl.(1) <- ft;
-  { norm = false; term = FOPN(MutCase ci,ncl) }
+let copy_case ci p ft bl =
+  (* Is the copy of bl necessary ?? I'd guess no HH *)
+  { norm = false; term = FCases (ci,p,ft,Array.copy bl) }
 
 
 (* Check if the case argument enables iota-reduction *)
 type case_status =
   | CONSTRUCTOR of int * fconstr array
-  | COFIX of int * int * fconstr array * fconstr array
+  | COFIX of int * int * (fconstr array * name list * fconstr array) *
+      fconstr array * constr array * freeze subs
   | IRREDUCTIBLE
 
 
 let constr_or_cofix env v =
   let (lft_hd, head, appl) = strip_freeze v in
   match head.term with
-    | FOPN(MutConstruct ((indsp,_),i),_) ->
+    | FConstruct (((indsp,_),i),_) ->
         let args = snd (array_chop (mindsp_nparams env indsp) appl) in
         CONSTRUCTOR (i, args)
-    | FOPN(CoFix bnum, bv) -> COFIX (lft_hd,bnum,bv,appl)
+    | FCoFix (bnum, def, bds, env) -> COFIX (lft_hd,bnum,def,appl, bds, env)
     | _ -> IRREDUCTIBLE
 
 let fix_reducible env unf_fun n appl =
@@ -880,41 +1061,73 @@ and whnf_frterm info ft =
       | FLIFT (k,f) ->
 	  let uf = unfreeze info f in
           { norm = uf.norm; term = FLIFT(k, uf) }
-      | FOP2 (Cast,f,_) -> whnf_frterm info f  (* remove outer casts *)
-      | FOPN (AppL,appl) -> whnf_apply info appl.(0) (array_tl appl)
-      | FOPN ((Const _ | Evar _) as op,vars) ->
-	  if red_under info.i_flags (DELTA op) then
-            let cst = DOPN(op, Array.map term_of_freeze vars) in
-            (match const_value_cache info cst with
+      | FCast (f,_) -> whnf_frterm info f  (* remove outer casts *)
+      | FApp (f,appl) -> whnf_apply info f appl
+      | FFlex (FConst sp,vars) ->
+	  if red_under info.i_flags (CONST [sp]) then
+            let cst = (sp, Array.map term_of_freeze vars) in
+            (match ref_value_cache info (ConstBinding cst) with
                | Some def ->
                    let udef = unfreeze info def in
                    lift_frterm 0 udef
                | None -> { norm = array_for_all is_val vars; term = ft.term })
 	  else 
 	    ft
-
-      | FOPN (MutCase ci,cl) ->
+      | FFlex (FEvar ev,vars) ->
+	  if red_under info.i_flags EVAR then
+            let ev = (ev, Array.map term_of_freeze vars) in
+            (match ref_value_cache info (EvarBinding ev) with
+               | Some def ->
+                   let udef = unfreeze info def in
+                   lift_frterm 0 udef
+               | None -> { norm = array_for_all is_val vars; term = ft.term })
+	  else 
+	    ft
+      | FFlex (FVar id, _) as t->
+	  if red_under info.i_flags DELTA then
+	    match ref_value_cache info (VarBinding id) with
+	      | Some def ->
+		  let udef = unfreeze info def in
+		  lift_frterm 0 udef
+	      | None -> { norm = true; term = t }
+	  else ft
+      | FFlex (FFarRel (n,k),_) as t ->
+	  if red_under info.i_flags DELTA then
+	    match ref_value_cache info (FarRelBinding k) with
+	      | Some def ->
+		  let udef = unfreeze info def in
+		  lift_frterm n udef
+	      | None -> { norm = true; term = t }
+	  else ft
+
+      | FCases (ci,p,co,bl) ->
 	  if red_under info.i_flags IOTA then
-            let c = unfreeze (infos_under info) cl.(1) in
+            let c = unfreeze (infos_under info) co in
             (match constr_or_cofix info.i_env c with
-	       | CONSTRUCTOR (n,real_args) when n <= (Array.length cl - 2) ->
-                   whnf_apply info cl.(n+1) real_args
-               | COFIX (lft_hd,bnum,bvect,appl) ->
-                   let cofix =
-                     contract_fix_vect (unfreeze info)
-                       (FOPN(CoFix bnum, bvect)) in
+	       | CONSTRUCTOR (n,real_args) when n <= Array.length bl ->
+                   whnf_apply info bl.(n-1) real_args
+               | COFIX (lft_hd,bnum,def,appl,bds,env) ->
+                   let cofix = contract_fix_vect (FCoFix (bnum,def,bds,env)) in
                    let red_cofix =
                      whnf_apply info (lift_freeze lft_hd cofix) appl in
-                   whnf_frterm info (copy_case ci cl red_cofix)
-               | _ -> { norm = array_for_all is_val cl; term = ft.term })
+                   whnf_frterm info (copy_case ci p red_cofix bl)
+               | _ ->
+		   { norm = is_val p & is_val co & array_for_all is_val bl;
+		     term = ft.term })
           else 
 	    ft
 
-      | FLet (na,b,_,_,t,subs) -> warning "Should be catch in whnf_term";
-	  contract_subst 0 t subs b
+      | FLetIn (na,b,fd,fc,d,subs) ->
+          let c = unfreeze info b in
+	  if red_under info.i_flags LETIN then
+	    contract_subst 0 d subs c
+	  else
+	    { norm = false;
+	      term = FLetIn (na,c,fd,fc,d,subs) }
+
+      | FRel _ | FAtom _ -> { norm = true; term = ft.term }
 
-      | FRel _ | FVAR _ | FOP0 _ -> { norm = true; term = ft.term }
-      | FOPN _ | FOP2 _ | FOP1 _ | FLam _ | FPrd _ | FLAM _ | FLAMV _ -> ft
+      | FFix _ | FCoFix _ | FInd _ | FConstruct _ | FLambda _ | FProd _ -> ft
 
 (* Weak head reduction: case of the application (head appl) *)
 and whnf_apply info head appl =
@@ -924,56 +1137,79 @@ and whnf_apply info head appl =
   else
     let (lft_hd,whd,args) = strip_frterm 0 head [appl] in
     match whd.term with
-      | FLam (_,_,_,t,subs) when red_under info.i_flags BETA ->
+      | FLambda (_,_,_,t,subs) when red_under info.i_flags BETA ->
           let vbody = contract_subst lft_hd t subs args.(0) in
           whnf_apply info vbody (array_tl args)
-      | (FOPN(Fix(reci,bnum), tb) as fx)
+      | FFix ((reci,bnum), _, _, _) as fx
           when red_under info.i_flags IOTA
             & fix_reducible info.i_env 
 	        (unfreeze (infos_under info)) reci.(bnum) args ->
-          let fix = contract_fix_vect (unfreeze info) fx in
+          let fix = contract_fix_vect fx in
           whnf_apply info (lift_freeze lft_hd fix) args
       | _ -> 
 	  { norm = (is_val head) & (array_for_all is_val appl);
-            term = FOPN(AppL, array_cons head appl) }
+            term = FApp (head, appl) }
 	    
 (* essayer whnf_frterm info (traverse_term env t) a la place?
  * serait moins lazy: traverse_term ne supprime pas les Cast a la volee, etc.
  *)
 and whnf_term info env t =
-  match t with
-    | Rel i -> (match expand_rel i env with
-		  | Inl (lams,v) ->
-		      let uv = unfreeze info v in
-		      lift_frterm lams uv
-		  | Inr k -> { norm = true; term = FRel k })
-    | VAR x -> { norm = true; term = FVAR x }
-    | DOP0 op -> {norm = true; term = FOP0 op }
-    | DOP1 (op, nt) -> { norm = false; term = FOP1 (op, freeze env nt) }
-    | DOP2 (Cast,ct,c) -> whnf_term info env ct    (* remove outer casts *)
-    | DOP2 (_,_,_) -> assert false (* Lambda|Prod made explicit *)
-    | DOPN ((AppL | Const _ | Evar _ | MutCase _) as op, ve) ->
-      	whnf_frterm info { norm = false; term = FOPN (op, freeze_vect env ve) }
-    | DOPN ((MutInd _ | MutConstruct _) as op,v) ->
-      	{ norm = (v=[||]); term = FOPN (op, freeze_vect env v) }
-    | DOPN (op,v) ->
-      	{ norm = false; term = FOPN (op, freeze_vect env v) } (* Fix CoFix *)
-    | DLAM (x,a) ->
-      	{ norm = false; term = FLAM (x, freeze (subs_lift env) a, a, env) }
-    | DLAMV (x,ve) ->
-      	{ norm = (ve=[||]);
-          term = FLAMV (x, freeze_vect (subs_lift env) ve, ve, env) }
-    | CLam (n,t,c) ->
+  match kind_of_term t with
+    | IsRel i ->
+	(match expand_rel i env with
+	   | Inl (lams,v) ->
+	       let uv = unfreeze info v in
+	       lift_frterm lams uv
+	   | Inr (n,None) ->
+	       { norm = true; term = FRel n }
+	   | Inr (n,Some k) ->
+	       whnf_frterm info
+		 { norm = false; term = FFlex (FFarRel (n,k), [||]) })
+
+    | IsVar x ->
+	whnf_frterm info { norm = false; term = FFlex (FVar x, [||]) }
+
+    | IsSort _ | IsXtra _ | IsMeta _ -> {norm = true; term = FAtom t }
+    | IsCast (c,_) -> whnf_term info env c    (* remove outer casts *)
+
+    | IsAppL (f,ve) ->
+      	whnf_frterm info
+	  { norm = false; term = FApp (freeze env f, freeze_vect env ve)}
+    | IsConst (op,ve) ->
+      	whnf_frterm info
+	  { norm = false; term = FFlex (FConst op, freeze_vect env ve) }
+    | IsEvar (op,ve) ->
+      	whnf_frterm info
+	  { norm = false; term = FFlex (FEvar op, freeze_vect env ve) }
+    | IsMutCase (ci,p,c,ve) ->
+      	whnf_frterm info
+	  { norm = false;
+	    term = FCases (ci, freeze env p, freeze env c, freeze_vect env ve)}
+
+    | IsMutInd (op,v) ->
+      	{ norm = (v=[||]); term = FInd (op, freeze_vect env v) }
+    | IsMutConstruct (op,v) ->
+      	{ norm = (v=[||]); term = FConstruct (op, freeze_vect env v) }
+
+    | IsFix (op,(_,_,bds as def)) ->
+      	{ norm = false; term = FFix (op, freeze_rec env def, bds, env) }
+    | IsCoFix (op,(_,_,bds as def)) ->
+      	{ norm = false; term = FCoFix (op, freeze_rec env def, bds, env) }
+
+    | IsLambda (n,t,c) ->
         { norm = false;
-	  term = FLam (n, typed_map (freeze env) t, freeze (subs_lift env) c,
+	  term = FLambda (n, freeze env t, freeze (subs_lift env) c,
 		       c, env) }
-    | CPrd (n,t,c)   ->
+    | IsProd (n,t,c)   ->
         { norm = false;
-	  term = FPrd (n, typed_map (freeze env) t, freeze (subs_lift env) c,
+	  term = FProd (n, freeze env t, freeze (subs_lift env) c,
 		       c, env) }
 
-    (* WHNF removes LetIn (see Paula Severi) *)
-    | CLet (n,b,t,c) ->	whnf_term info (subs_cons (freeze env b,env)) c
+    | IsLetIn (n,b,t,c) -> 
+      	whnf_frterm info
+          { norm = false;
+	    term = FLetIn (n, freeze env b, freeze env t,
+			   freeze (subs_lift env) c, c, env) }
 
 (* parameterized norm *)
 let norm_val info v =
@@ -989,19 +1225,30 @@ let whd_val info v =
   let uv = unfreeze info v in
   term_of_freeze uv
 
-let search_frozen_cst info op vars =
-  let cst = DOPN(op, Array.map (norm_val info) vars) in
-  const_value_cache info cst
-    
+let inject = freeze (ESID 0)
+
+let search_frozen_value info f vars = match f with
+  | FConst op ->
+      ref_value_cache info (ConstBinding (op,Array.map (norm_val info) vars))
+  | FEvar op ->
+      ref_value_cache info (EvarBinding (op,Array.map (norm_val info) vars))
+  | FVar id ->
+      ref_value_cache info (VarBinding id)
+  | FFarRel (n,p) ->
+      ref_value_cache info (FarRelBinding (n+p))
+
 
 (* cache of constants: the body is computed only when needed. *)
 type 'a clos_infos = (fconstr, 'a) infos
 
+
 let create_clos_infos flgs env sigma =
   { i_flags = flgs;
-    i_repr = (fun old_info c -> inject c);
+    i_repr = (fun old_info n c -> freeze (ESID (-n)) c);
     i_env = env;
     i_evc = sigma;
+    i_rels = defined_rels flgs env;
+    i_vars = defined_vars flgs env;
     i_tab = Hashtbl.create 17 }
 
 let clos_infos_env infos = infos.i_env
diff --git a/kernel/closure.mli b/kernel/closure.mli
index d9353abfa2..14107f56db 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -15,21 +15,36 @@ val stats : bool ref
 val share : bool ref
 
 
-(*s The set of reduction kinds. *)
-type red_kind = BETA | DELTA of sorts oper | IOTA
 
-type reds = { 
-  r_beta : bool;
-  r_delta : sorts oper -> bool;
-  r_iota : bool }
+(*s Delta implies all consts (both global (= by
+  section_path) and local (= by Rel or Var)), all evars, and letin's.
+  Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
+  a LetIn expression is Letin reduction *)
+
+type red_kind =
+  | BETA
+  | DELTA
+  | LETIN
+  | EVAR
+  | IOTA
+  | CONST of section_path list
+  | CONSTBUT of section_path list
+
+(* Sets of reduction kinds. *)
+type reds
 
 val no_red : reds
 val beta_red : reds
 val betaiota_red : reds
 val betadeltaiota_red : reds
+val unfold_red : section_path -> reds
 
+(* Tests if a reduction kind is set *)
 val red_set : reds -> red_kind -> bool
 
+(* Adds a reduction kind to a set *)
+val red_add : reds -> red_kind -> reds
+
 
 (*s Reduction function specification. *)
 
@@ -53,13 +68,14 @@ val betaiota : flags
 val betadeltaiota : flags
 
 val hnf_flags : flags
+val unfold_flags : section_path -> flags
 
-(*s Explicit substitutions of type ['a]. [ESID] = identity. 
+(*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity. 
   [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
   $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. 
   [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
 type 'a subs =
-  | ESID
+  | ESID of int
   | CONS of 'a * 'a subs
   | SHIFT of int * 'a subs
   | LIFT of int * 'a subs
@@ -104,7 +120,7 @@ val cbv_norm : 'a cbv_infos -> constr -> constr
 val cbv_stack_term : 'a cbv_infos ->
   stack -> cbv_value subs -> constr -> cbv_value
 val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr
-val cbv_norm_more : 'a cbv_infos -> cbv_value -> cbv_value
+val cbv_norm_more : 'a cbv_infos -> cbv_value subs -> cbv_value -> cbv_value
 val norm_head : 'a cbv_infos ->
   cbv_value subs -> constr -> stack -> cbv_value * stack
 val apply_stack : 'a cbv_infos -> constr -> stack -> constr
@@ -113,24 +129,34 @@ val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
 
 (*s Lazy reduction. *)
 
-type freeze
+type freeze = { 
+  mutable norm: bool; 
+  mutable term: frterm }
 
-type frterm =
+and frterm =
   | FRel of int
-  | FVAR of identifier
-  | FOP0 of sorts oper
-  | FOP1 of sorts oper * freeze
-  | FOP2 of sorts oper * freeze * freeze
-  | FOPN of sorts oper * freeze array
-  | FLAM of name * freeze * constr * freeze subs
-  | FLAMV of name * freeze array * constr array * freeze subs
-  | FLam of name * type_freeze * freeze * constr * freeze subs
-  | FPrd of name * type_freeze * freeze * constr * freeze subs
-  | FLet of name * freeze * type_freeze * freeze * constr * freeze subs
+  | FAtom of constr
+  | FCast of freeze * freeze
+  | FFlex of frreference * freeze array
+  | FInd of inductive_path * freeze array
+  | FConstruct of constructor_path * freeze array
+  | FApp of freeze * freeze array
+  | FFix of (int array * int) * (freeze array * name list * freeze array)
+      * constr array * freeze subs
+  | FCoFix of int * (freeze array * name list * freeze array)
+      * constr array * freeze subs
+  | FCases of case_info * freeze * freeze * freeze array
+  | FLambda of name * freeze * freeze * constr * freeze subs
+  | FProd of name * freeze * freeze * constr * freeze subs
+  | FLetIn of name * freeze * freeze * freeze * constr * freeze subs
   | FLIFT of int * freeze
   | FFROZEN of constr * freeze subs
 
-and type_freeze = freeze
+and frreference =
+  | FConst of section_path
+  | FEvar of existential_key
+  | FVar of identifier
+  | FFarRel of int * int
 
 val frterm_of : freeze -> frterm
 val is_val : freeze -> bool
@@ -153,9 +179,14 @@ val applist_of_freeze : freeze array -> constr list
 (* contract a substitution *)
 val contract_subst : int -> constr -> freeze subs -> freeze -> freeze
 
+(* Global and local constant cache *)
+type 'a clos_infos
+val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos
+val clos_infos_env : 'a clos_infos -> env
 
 (* Calculus of Constructions *)
 type fconstr = freeze
+
 val inject : constr -> fconstr
 
 val strip_frterm :
@@ -164,30 +195,26 @@ val strip_freeze : fconstr -> int * fconstr * fconstr array
 
 
 (* Auxiliary functions for (co)fixpoint reduction *)
-val contract_fix_vect : (fconstr -> fconstr) -> frterm -> fconstr
-val copy_case : case_info -> fconstr array -> fconstr -> fconstr
+val contract_fix_vect : frterm -> fconstr
+val copy_case : case_info -> fconstr -> fconstr -> fconstr array -> fconstr
 
 
 (* Iota analysis: reducible ? *)
 type case_status =
   | CONSTRUCTOR of int * fconstr array
-  | COFIX of int * int * fconstr array * fconstr array
+  | COFIX of int * int * (fconstr array * name list * fconstr array) *
+      fconstr array * constr array * freeze subs
   | IRREDUCTIBLE
 
 
-(* Constant cache *)
-type 'a clos_infos
-val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos
-val clos_infos_env : 'a clos_infos -> env
-
 (* Reduction function *)
 val norm_val : 'a clos_infos -> fconstr -> constr
 val whd_val : 'a clos_infos -> fconstr -> constr
 val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr array
 val fhnf_apply : 'a clos_infos ->
   int -> fconstr -> fconstr array -> int * fconstr * fconstr array
-val search_frozen_cst : 'a clos_infos ->
-  sorts oper -> fconstr array -> fconstr option
+val search_frozen_value : 
+  'a clos_infos -> frreference -> fconstr array -> fconstr option
 
 (* recursive functions... *)
 val unfreeze : 'a clos_infos -> fconstr -> fconstr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c811af2dbe..c353e47657 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -13,7 +13,6 @@ open Environ
 open Instantiate
 open Closure
 
-exception Redelimination
 exception Elimconst
 
 (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) 
@@ -114,33 +113,7 @@ let strong whdfun env sigma =
   strongrec
 
 let local_strong whdfun = 
-  let rec strongrec t = map_constr strongrec (whdfun t)
-
-(*
-match whdfun t with
-    | DOP0 _ as t -> t
-    | DOP1(oper,c) -> DOP1(oper,strongrec c)
-    | DOP2(oper,c1,c2) -> DOP2(oper,strongrec c1,strongrec c2)
-    (* Cas ad hoc *)
-    | DOPN(Fix _ as oper,cl) ->
-	let cl' = Array.copy cl in
-	let l = Array.length cl -1 in
-	for i=0 to l-1 do cl'.(i) <- strongrec cl.(i) done;
-	cl'.(l) <- strongrec_lam cl.(l);
-	DOPN(oper, cl')	
-    | DOPN(oper,cl) -> DOPN(oper,Array.map strongrec cl)
-    | CLam(n,t,c)   -> CLam (n, typed_app strongrec t, strongrec c)  
-    | CPrd(n,t,c)   -> CPrd (n, typed_app strongrec t, strongrec c)
-    | CLet(n,b,t,c) -> CLet (n, strongrec b,typed_app strongrec t, strongrec c)
-    | VAR _ as t -> t
-    | Rel _ as t -> t
-    | DLAM _ | DLAMV _ -> assert false
-  and strongrec_lam = function
-    | DLAM(na,c) -> DLAM(na,strongrec_lam c)
-    | DLAMV(na,c) -> DLAMV(na,Array.map strongrec c)
-    | _ -> assert false
-*)
-  in
+  let rec strongrec t = map_constr strongrec (whdfun t) in
   strongrec
 
 let rec strong_prodspine redfun c = 
@@ -153,18 +126,6 @@ let rec strong_prodspine redfun c =
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
 
-
-(* call by value reduction functions *)
-let cbv_norm_flags flags env sigma t =
-  cbv_norm (create_cbv_infos flags env sigma) t
-
-let cbv_beta env = cbv_norm_flags beta env
-let cbv_betaiota env = cbv_norm_flags betaiota env
-let cbv_betadeltaiota env =  cbv_norm_flags betadeltaiota env
-
-let compute = cbv_betadeltaiota
-
-
 (* lazy reduction functions. The infos must be created for each term *)
 let clos_norm_flags flgs env sigma t =
   norm_val (create_clos_infos flgs env sigma) (inject t)
@@ -173,171 +134,11 @@ let nf_beta env = clos_norm_flags beta env
 let nf_betaiota env = clos_norm_flags betaiota env
 let nf_betadeltaiota env =  clos_norm_flags betadeltaiota env
 
-
 (* lazy weak head reduction functions *)
 (* Pb: whd_val parcourt tout le terme, meme si aucune reduction n'a lieu *)
 let whd_flags flgs env sigma t =
   whd_val (create_clos_infos flgs env sigma) (inject t)
 
-
-(* Red reduction tactic: reduction to a product *)
-let red_product env sigma c = 
-  let rec redrec x =
-    match kind_of_term x with
-      | IsAppL (f,l) -> appvect (redrec f, l)
-      | IsConst (_,_) when evaluable_constant env x -> constant_value env x
-      | IsEvar (ev,args) when Evd.is_defined sigma ev -> 
-	  existential_value sigma (ev,args)
-      | IsCast (c,_) -> redrec c
-      | IsProd (x,a,b) -> mkProd (x, a, redrec b)
-      | _ -> error "Term not reducible"
-  in 
-  nf_betaiota env sigma (redrec c)
-
-(* 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 kind_of_term c with
-    | IsConst (sp,_) when sp = name ->
-        if List.hd ol = n then
-          if evaluable_constant env c then 
-	    (n+1, List.tl ol, constant_value env c)
-          else
-            errorlabstrm "substlin"
-              [< print_sp sp; 'sTR " is not a defined constant" >]
-        else 
-	  ((n+1),ol,c)
-
-    (* INEFFICIENT: OPTIMIZE *)
-    | IsAppL (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
-
-    | IsLambda (na,c1,c2) ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkLambda (na,c1',c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkLambda (na,c1',c2')))
-
-    | IsLetIn (na,c1,t,c2) ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkLambda (na,c1',c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkLambda (na,c1',c2')))
-
-    | IsProd (na,c1,c2) ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkProd (na,c1',c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkProd (na,c1',c2')))
-	
-    | IsMutCase (ci,p,d,llf) -> 
-        let rec substlist nn oll = function
-          | []     -> (nn,oll,[])
-          | f::lfe ->
-              let (nn1,oll1,f') = substlin env name nn oll f in
-              (match oll1 with
-                 | [] -> (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 *)
-        (match ol1 with                                 (* si P pas affiche *)
-           | [] -> (n1,[],mkMutCase (ci, p', d, llf))
-           | _  ->
-               let (n2,ol2,d') = substlin env name n1 ol1 d in
-               (match ol2 with
-		  | [] -> (n2,[],mkMutCase (ci, p', d', llf))
-		  | _  -> 
-	              let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf)
-                      in (n3,ol3,mkMutCaseL (ci, p', d', lf'))))
-        
-    | IsCast (c1,c2)   ->
-        let (n1,ol1,c1') = substlin env name n ol c1 in
-        (match ol1 with 
-           | [] -> (n1,[],mkCast (c1',c2))
-           | _  ->
-               let (n2,ol2,c2') = substlin env name n1 ol1 c2 in
-               (n2,ol2,mkCast (c1',c2')))
-
-    | IsFix _ -> 
-        (warning "do not consider occurrences inside fixpoints"; (n,ol,c))
-	
-    | IsCoFix _ -> 
-        (warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
-
-    | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _
-      |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c)
-	
-	  
-let unfold env sigma name =
-  let flag = 
-    (UNIFORM,{ r_beta = true;
-               r_delta = (fun op -> op=(Const name));
-               r_iota = true })
-  in 
-  clos_norm_flags flag env sigma
-
-
-(* unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)
- * Unfolds the constant name in a term c following a list of occurrences occl.
- * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
- * Performs a betaiota reduction after unfolding. *)
-let unfoldoccs env sigma (occl,name) c =
-  match occl with
-    | []  -> unfold env sigma name c
-    | l -> 
-        match substlin env name 1 (Sort.list (<) l) c with
-          | (_,[],uc) -> nf_betaiota env sigma 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 sigma c = 
-  List.fold_left (fun c occname -> unfoldoccs env sigma occname c) c loccname
-
-(* Re-folding constants tactics: refold com in term c *)
-let fold_one_com com env sigma c =
-  let rcom = red_product env sigma com in
-  subst1 com (subst_term rcom c)
-
-let fold_commands cl env sigma c =
-  List.fold_right (fun com -> fold_one_com com env sigma) (List.rev cl) c
-
-
-(* Pattern *)
-
-(* 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 error "cannot find a type for the generalisation";
-  if occur_meta a then 
-    mkLambda (na,ta,t)
-  else 
-    mkLambda (na, ta,subst_term_occ locc a t)
-
-
-let pattern_occs loccs_trm_typ env sigma 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)
-
-
 (*************************************)
 (*** Reduction using substitutions ***)
 (*************************************)
@@ -462,10 +263,14 @@ let reduce_fix whdfun fix stack =
 let whd_state_gen flags env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsEvar (ev,args) when red_evar flags & Evd.is_defined sigma ev ->
-	  whrec (existential_value sigma (ev,args), stack)
-      | IsConst _ when red_delta flags & evaluable_constant env x ->
-	  whrec (constant_value env x, stack)
+      | IsEvar ev when red_evar flags ->
+	  (match existential_opt_value sigma ev with
+	     | Some  body -> whrec (body, stack)
+	     | None -> s)
+      | IsConst const when red_delta flags ->
+	  (match constant_opt_value env const with
+	     | Some  body -> whrec (body, stack)
+	     | None -> s)
       | IsLetIn (_,b,_,c) when red_delta flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
       | IsAppL (f,cl)  -> whrec (f, append_stack cl stack)
@@ -576,8 +381,8 @@ let whd_beta x = app_stack (whd_beta_state (x,empty_stack))
 let whd_delta_state env sigma = 
   let rec whrec (x, l as s) =
     match kind_of_term x with
-      | IsConst _ when evaluable_constant env x ->
-	  whrec (constant_value env x, l)
+      | IsConst const when evaluable_constant env x ->
+	  whrec (constant_value env const, l)
       | IsEvar (ev,args) when Evd.is_defined sigma ev ->
           whrec (existential_value sigma (ev,args), l)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
@@ -598,9 +403,9 @@ let whd_delta env sigma c =
 let whd_betadelta_state env sigma = 
   let rec whrec (x, l as s) =
     match kind_of_term x with
-      | IsConst _ ->
+      | IsConst const ->
           if evaluable_constant env x then 
-	    whrec (constant_value env x, l)
+	    whrec (constant_value env const, l)
           else 
 	    s
       | IsEvar (ev,args) ->
@@ -657,8 +462,8 @@ let whd_betaevar env sigma c =
 let whd_betadeltaeta_state env sigma = 
   let rec whrec (x, l as s) =
     match kind_of_term x with
-      | IsConst _ when evaluable_constant env x ->
-	  whrec (constant_value env x, l)
+      | IsConst const when evaluable_constant env x ->
+	  whrec (constant_value env const, l)
       | IsEvar (ev,args) when Evd.is_defined sigma ev ->
 	  whrec (existential_value sigma (ev,args), l)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
@@ -775,8 +580,8 @@ let whd_betaiotaevar env sigma x =
 let whd_betadeltaiota_state env sigma =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsConst _ when evaluable_constant env x ->
-	  whrec (constant_value env x, stack)
+      | IsConst const when evaluable_constant env x ->
+	  whrec (constant_value env const, stack)
       | IsEvar (ev,args) when Evd.is_defined sigma ev ->
 	  whrec (existential_value sigma (ev,args), stack)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
@@ -813,8 +618,8 @@ let whd_betadeltaiota env sigma x =
 let whd_betadeltaiotaeta_state env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsConst _ when evaluable_constant env x ->
-	  whrec (constant_value env x, stack)
+      | IsConst const when evaluable_constant env x ->
+	  whrec (constant_value env const, stack)
       | IsEvar (ev,args) when Evd.is_defined sigma ev -> 
 	  whrec (existential_value sigma (ev,args), stack)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
@@ -887,8 +692,8 @@ exception NotConvertible
 let convert_of_bool b c =
   if b then c else raise NotConvertible
 
-let bool_and_convert b f = 
-  if b then f else fun _ -> raise NotConvertible
+let bool_and_convert b f c = 
+  if b then f c else raise NotConvertible
 
 let convert_and f1 f2 c = f2 (f1 c)
 
@@ -933,83 +738,70 @@ and eqappr cv_pb infos appr1 appr2 =
   and el2 = el_shft n2 lft2 in
   match (frterm_of hd1, frterm_of hd2) with
     (* case of leaves *)
-    | (FOP0(Sort s1), FOP0(Sort s2)) -> 
-	bool_and_convert
-	  (Array.length v1 = 0 && Array.length v2 = 0)
-	  (sort_cmp cv_pb s1 s2)
-	  
-    | (FVAR x1, FVAR x2) ->
-	bool_and_convert (x1=x2)
-	  (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
-
+    | (FAtom a1, FAtom a2) ->
+	(match kind_of_term a1, kind_of_term a2 with
+	   | (IsSort s1, IsSort s2) -> 
+	       bool_and_convert
+		 (Array.length v1 = 0 && Array.length v2 = 0)
+		 (sort_cmp cv_pb s1 s2)
+	   | (IsMeta n, IsMeta m) ->
+               bool_and_convert (n=m) 
+		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		    v1 v2)
+	   | IsXtra s1, IsXtra s2 ->
+               bool_and_convert (s1=s2)
+		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		    v1 v2)
+	   | _ -> fun _ -> raise NotConvertible)
+
+    (* 2 index known to be bound to no constant *)
     | (FRel n, FRel m) ->
         bool_and_convert 
-	  (reloc_rel n el1 = reloc_rel m el2)
+          (reloc_rel n el1 = reloc_rel m el2)
           (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
 
-    | (FOP0(Meta n), FOP0(Meta m)) ->
-        bool_and_convert (n=m) 
-	  (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
-
-    (* 2 constants, 2 existentials or 2 abstractions *)
-    | (FOPN(Const sp1,al1), FOPN(Const sp2,al2)) ->
-	convert_or
-	  (* try first intensional equality *)
-	  (bool_and_convert (sp1 == sp2 or sp1 = sp2)
-	     (convert_and
-		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
-		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
-		   v1 v2)))
-          (* else expand the second occurrence (arbitrary heuristic) *)
-          (match search_frozen_cst infos (Const sp2) al2 with
-             | Some def2 -> 
-		 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 _ -> raise NotConvertible))
-
-    | (FOPN(Evar ev1,al1), FOPN(Evar ev2,al2)) ->
+    (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *)
+    | (FFlex (fl1,al1), FFlex (fl2,al2)) ->
 	convert_or
 	  (* try first intensional equality *)
-	  (bool_and_convert (ev1 == ev2)
+	  (bool_and_convert (fl1 = fl2)
 	     (convert_and
 		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2)
 		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
 		   v1 v2)))
           (* else expand the second occurrence (arbitrary heuristic) *)
-          (match search_frozen_cst infos (Evar ev2) al2 with
+          (fun u ->
+	     match search_frozen_value infos fl2 al2 with
              | Some def2 -> 
-		 eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
-             | None -> (match search_frozen_cst infos (Evar ev1) al1 with
+		 eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) u
+             | None -> (match search_frozen_value infos fl1 al1 with
                           | Some def1 -> eqappr cv_pb infos
-				(lft1, fhnf_apply infos n1 def1 v1) appr2
-			  | None -> fun _ -> raise NotConvertible))
+				(lft1, fhnf_apply infos n1 def1 v1) appr2 u
+			  | None -> raise NotConvertible))
 
-    (* only one constant, existential or abstraction *)
-    | (FOPN((Const _ | Evar _) as op,al1), _)      ->
-        (match search_frozen_cst infos op al1 with
+    (* only one constant, existential, defined var or defined rel *)
+    | (FFlex (fl1,al1), _)      ->
+        (match search_frozen_value infos fl1 al1 with
            | Some def1 -> 
 	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2
            | None -> fun _ -> raise NotConvertible)
-
-    | (_, FOPN((Const _ | Evar _) as op,al2))      ->
-        (match search_frozen_cst infos op al2 with
+    | (_, FFlex (fl2,al2))      ->
+        (match search_frozen_value infos fl2 al2 with
            | Some def2 -> 
 	       eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
            | None -> fun _ -> raise NotConvertible)
 	
     (* other constructors *)
-    | (FLam (_,c1,c2,_,_), FLam (_,c'1,c'2,_,_)) ->
+    | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,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 (el_lift el1) (el_lift el2) c2 c'2))
 
-    | (FLet _, _) | (_, FLet _) -> anomaly "Normally removed by fhnf"
+    | (FLetIn _, _) | (_, FLetIn _) -> anomaly "Normally removed by fhnf"
 
-    | (FPrd (_,c1,c2,_,_), FPrd (_,c'1,c'2,_,_)) ->
+    | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) ->
 	bool_and_convert
           (Array.length v1 = 0 && Array.length v2 = 0)
 	  (convert_and
@@ -1018,32 +810,50 @@ and eqappr cv_pb infos appr1 appr2 =
 
     (* Inductive types:  MutInd MutConstruct MutCase Fix Cofix *)
 
-         (* Le cas MutCase doit venir avant le cas general DOPN car, a
-            priori, 2 termes a base de MutCase peuvent etre convertibles
-            sans que les annotations des MutCase le soient *)
+      (* Les annotations du MutCase ne servent qu'à l'affichage *)
 
-    | (FOPN(MutCase _,cl1), FOPN(MutCase _,cl2)) ->
-        convert_and
-	  (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
-          (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+    | (FCases (_,p1,c1,cl1), FCases (_,p2,c2,cl2)) ->
+	convert_and
+	  (ccnv (pb_equal cv_pb) infos el1 el2 p1 p2)
+	  (convert_and
+	     (ccnv (pb_equal cv_pb) infos el1 el2 c1 c2)
+	     (convert_and
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
+		(convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)
+	     ))
 
-     | (FOPN(op1,cl1), FOPN(op2,cl2)) ->
+     | (FInd (op1,cl1), FInd(op2,cl2)) ->
 	 bool_and_convert (op1 = op2)
 	   (convert_and
               (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
               (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
-
-     (* binders *)
-     | (FLAM(_,c1,_,_), FLAM(_,c2,_,_)) ->
-	 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,_,_)) ->
-	 bool_and_convert
-           (Array.length v1 = 0 & Array.length v2 = 0)
-           (convert_forall2 
-	      (ccnv cv_pb infos (el_lift el1) (el_lift el2)) vc1 vc2)
+     | (FConstruct (op1,cl1), FConstruct(op2,cl2)) ->
+	 bool_and_convert (op1 = op2)
+	   (convert_and
+              (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2)
+              (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
+     | (FFix (op1,(tys1,_,cl1),_,_), FFix(op2,(tys2,_,cl2),_,_)) ->
+	 let n = Array.length cl1 in
+	 bool_and_convert (op1 = op2)
+	   (convert_and
+              (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) tys1 tys2)
+	      (convert_and
+		 (convert_forall2 (ccnv (pb_equal cv_pb) infos 
+				     (el_liftn n el1) (el_liftn n el2))
+		    cl1 cl2)
+		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		    v1 v2)))
+     | (FCoFix (op1,(tys1,_,cl1),_,_), FCoFix(op2,(tys2,_,cl2),_,_)) ->
+	 let n = Array.length cl1 in
+	 bool_and_convert (op1 = op2)
+	   (convert_and
+              (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) tys1 tys2)
+	      (convert_and
+		 (convert_forall2 (ccnv (pb_equal cv_pb) infos
+				     (el_liftn n el1) (el_liftn n el2))
+		    cl1 cl2)
+		 (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2)
+		    v1 v2)))
 
      | _ -> (fun _ -> raise NotConvertible)
 
@@ -1055,7 +865,8 @@ let fconv cv_pb env sigma t1 t2 =
     Constraint.empty
   else
     let infos = create_clos_infos hnf_flags env sigma in
-    ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
+    ccnv cv_pb infos ELID ELID (inject t1) (inject t2)
+      Constraint.empty
 
 let conv env = fconv CONV env
 let conv_leq env = fconv CONV_LEQ env 
@@ -1083,9 +894,9 @@ let is_fconv = function | CONV -> is_conv | CONV_LEQ -> is_conv_leq
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta metamap = function
-  | DOP0(Meta p) as u -> (try List.assoc p metamap with Not_found -> u)
-  | x -> x
+let whd_meta metamap c = match kind_of_term c with
+  | IsMeta p -> (try List.assoc p metamap with Not_found -> c)
+  | _ -> c
 	
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
@@ -1148,8 +959,9 @@ let sort_of_arity env c = snd (splay_arity env Evd.empty c)
   
 let decomp_n_prod env sigma n = 
   let rec decrec m ln c = if m = 0 then (ln,c) else 
-    match whd_betadeltaiota env sigma c with
-      | CPrd (n,a,c0) ->
+    match kind_of_term (whd_betadeltaiota env sigma c) with
+      | IsProd (n,a,c0) ->
+	  let a = make_typed_lazy a (fun _ -> Type dummy_univ) in
 	  decrec (m-1) (Sign.add_rel_decl (n,a) ln) c0
       | _                      -> error "decomp_n_prod: Not enough products"
   in 
@@ -1180,8 +992,8 @@ let compute_consteval env sigma c =
 	  let p = Array.length tys in
           let li = 
             List.map
-	      (function
-                 | Rel k
+	      (function c -> match kind_of_term c with
+                 | IsRel k
 		     when (array_for_all (noccurn k) tys
 			   & array_for_all (noccurn (k+p)) bds)
 		       -> (k, List.nth labs (k-1)) 
@@ -1193,7 +1005,7 @@ let compute_consteval env sigma c =
           else 
 	    raise Elimconst
 
-      | IsMutCase (_,_,Rel _,_), _ -> ([],n,false)
+      | IsMutCase (_,_,c,_), _ when isRel c -> ([],n,false)
 
       | _ -> raise Elimconst
   in
@@ -1317,28 +1129,6 @@ let add_free_rels_until bound m acc =
   in 
   frec 1 acc m 
 
-(*
-let add_free_rels_until bound m acc =
-  let rec frec depth acc = function
-    | Rel n -> 
-	if (n < bound+depth) & (n >= depth) then
-	  Intset.add (bound+depth-n) acc
-	else
-	  acc
-    | DOPN(_,cl)    -> Array.fold_left (frec depth) acc cl
-    | DOP2(_,c1,c2) -> frec depth (frec depth acc c1) c2
-    | DOP1(_,c)     -> frec depth acc c
-    | DLAM(_,c)     -> frec (depth+1) acc c
-    | DLAMV(_,cl)   -> Array.fold_left (frec (depth+1)) acc cl
-    | CLam (_,t,c)   -> frec (depth+1) (frec depth acc (body_of_type t)) c
-    | CPrd (_,t,c)   -> frec (depth+1) (frec depth acc (body_of_type t)) c
-    | CLet (_,b,t,c) -> frec (depth+1) (frec depth (frec depth acc b) (body_of_type t)) c
-    | VAR _         -> acc
-    | DOP0 _        -> acc
-  in 
-  frec 1 acc m 
-*)
-
 (* calcule la liste des arguments implicites *)
 
 let poly_args env sigma t =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index bc004aec65..d1a092ae7f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -13,7 +13,6 @@ open Closure
 
 (* Reduction Functions. *)
 
-exception Redelimination
 exception Elimconst
 
 (*s A [stack] is a context of arguments, arguments are pushed by
@@ -58,22 +57,15 @@ val stack_reduction_of_reduction :
 i*)
 val stacklam : (state -> 'a) -> constr list -> constr -> stack -> 'a 
 
-(*s Generic Optimized Reduction Functions using Closures *)
+(*s Generic Optimized Reduction Function using Closures *)
 
-(* 1. lazy strategy *)
 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 : 'a reduction_function
 
-(* 2. call by value strategy *)
-val cbv_norm_flags : flags -> 'a reduction_function
-val cbv_beta : 'a reduction_function
-val cbv_betaiota : 'a reduction_function
-val cbv_betadeltaiota : 'a reduction_function
-
-(* 3. lazy strategy, weak head reduction *)
+(* Lazy strategy, weak head reduction *)
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betadeltaiota : 'a contextual_reduction_function
@@ -147,13 +139,6 @@ val poly_args : env -> 'a evar_map -> constr -> int list
 
 val whd_programs : 'a reduction_function
 
-val unfoldn : 
-  (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 pattern_occs : (int list * constr * constr) list -> 'a reduction_function
-val compute : 'a reduction_function
-
 (* [reduce_fix] contracts a fix redex if it is actually reducible *)
 
 type fix_reduction_result = NotReducible | Reduced of state
@@ -231,4 +216,4 @@ val whd_ise1_metas : 'a evar_map -> constr -> constr
 val hnf : env -> 'a evar_map -> constr -> constr * constr list
 i*)
 val apprec : 'a state_reduction_function
-val red_product : 'a reduction_function
+