nouvelle implantation de la reduction

suppression de IsXtra du noyau


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

26 files changed, 1350 insertions, 1275 deletions

diff --git a/.depend b/.depend
index 32b6293a5..4ff2a8547 100644
--- a/.depend
+++ b/.depend
@@ -1,11 +1,12 @@
-kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/term.cmi 
+kernel/closure.cmi: kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \
+    kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi 
 kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
 kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
+kernel/esubst.cmi: lib/util.cmi 
 kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 kernel/indtypes.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
@@ -78,6 +79,8 @@ parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     kernel/inductive.cmi kernel/names.cmi pretyping/rawterm.cmi \
     kernel/term.cmi 
+pretyping/cbv.cmi: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \
+    kernel/evd.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     library/libobject.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 pretyping/coercion.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
@@ -224,10 +227,10 @@ dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
     proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \
     proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx kernel/univ.cmx \
     toplevel/vernacentries.cmx toplevel/vernacinterp.cmx 
-kernel/closure.cmo: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
+kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \
     kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
     kernel/univ.cmi lib/util.cmi kernel/closure.cmi 
-kernel/closure.cmx: kernel/declarations.cmx kernel/environ.cmx kernel/evd.cmx \
+kernel/closure.cmx: kernel/environ.cmx kernel/esubst.cmx kernel/evd.cmx \
     kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
     kernel/univ.cmx lib/util.cmx kernel/closure.cmi 
 kernel/cooking.cmo: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -246,6 +249,8 @@ kernel/environ.cmo: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \
 kernel/environ.cmx: kernel/declarations.cmx kernel/names.cmx lib/pp.cmx \
     kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     kernel/environ.cmi 
+kernel/esubst.cmo: lib/util.cmi kernel/esubst.cmi 
+kernel/esubst.cmx: lib/util.cmx kernel/esubst.cmi 
 kernel/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
     kernel/evd.cmi 
 kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
@@ -275,13 +280,13 @@ kernel/instantiate.cmx: kernel/declarations.cmx kernel/environ.cmx \
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi 
 kernel/reduction.cmo: kernel/closure.cmi kernel/declarations.cmi \
-    kernel/environ.cmi kernel/evd.cmi kernel/instantiate.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
-    kernel/reduction.cmi 
+    kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \
+    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/reduction.cmi 
 kernel/reduction.cmx: kernel/closure.cmx kernel/declarations.cmx \
-    kernel/environ.cmx kernel/evd.cmx kernel/instantiate.cmx kernel/names.cmx \
-    lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
-    kernel/reduction.cmi 
+    kernel/environ.cmx kernel/esubst.cmx kernel/evd.cmx \
+    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/reduction.cmi 
 kernel/safe_typing.cmo: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi kernel/indtypes.cmi \
     kernel/inductive.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
@@ -298,10 +303,10 @@ kernel/sign.cmo: kernel/names.cmi lib/options.cmi kernel/term.cmi \
     lib/util.cmi kernel/sign.cmi 
 kernel/sign.cmx: kernel/names.cmx lib/options.cmx kernel/term.cmx \
     lib/util.cmx kernel/sign.cmi 
-kernel/term.cmo: lib/hashcons.cmi kernel/names.cmi lib/pp.cmi kernel/univ.cmi \
-    lib/util.cmi kernel/term.cmi 
-kernel/term.cmx: lib/hashcons.cmx kernel/names.cmx lib/pp.cmx kernel/univ.cmx \
-    lib/util.cmx kernel/term.cmi 
+kernel/term.cmo: kernel/esubst.cmi lib/hashcons.cmi kernel/names.cmi \
+    lib/pp.cmi kernel/univ.cmi lib/util.cmi kernel/term.cmi 
+kernel/term.cmx: kernel/esubst.cmx lib/hashcons.cmx kernel/names.cmx \
+    lib/pp.cmx kernel/univ.cmx lib/util.cmx kernel/term.cmi 
 kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/type_errors.cmi 
@@ -582,6 +587,14 @@ pretyping/cases.cmx: pretyping/coercion.cmx kernel/declarations.cmx \
     pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
     pretyping/cases.cmi 
+pretyping/cbv.cmo: kernel/closure.cmi kernel/declarations.cmi \
+    kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \
+    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+    kernel/univ.cmi lib/util.cmi pretyping/cbv.cmi 
+pretyping/cbv.cmx: kernel/closure.cmx kernel/declarations.cmx \
+    kernel/environ.cmx kernel/esubst.cmx kernel/evd.cmx \
+    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+    kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi 
 pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     library/global.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \
     lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi pretyping/retyping.cmi \
@@ -686,14 +699,14 @@ pretyping/syntax_def.cmo: library/lib.cmi library/libobject.cmi \
 pretyping/syntax_def.cmx: library/lib.cmx library/libobject.cmx \
     kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmx \
     library/summary.cmx pretyping/syntax_def.cmi 
-pretyping/tacred.cmo: kernel/closure.cmi library/declare.cmi \
-    kernel/environ.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi library/summary.cmi \
-    kernel/term.cmi lib/util.cmi pretyping/tacred.cmi 
-pretyping/tacred.cmx: kernel/closure.cmx library/declare.cmx \
-    kernel/environ.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    kernel/names.cmx lib/pp.cmx kernel/reduction.cmx library/summary.cmx \
-    kernel/term.cmx lib/util.cmx pretyping/tacred.cmi 
+pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi \
+    library/declare.cmi kernel/environ.cmi kernel/inductive.cmi \
+    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+    library/summary.cmi kernel/term.cmi lib/util.cmi pretyping/tacred.cmi 
+pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \
+    library/declare.cmx kernel/environ.cmx kernel/inductive.cmx \
+    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+    library/summary.cmx kernel/term.cmx lib/util.cmx pretyping/tacred.cmi 
 pretyping/typing.cmo: kernel/environ.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
     kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi 
diff --git a/Makefile b/Makefile
index 2de7a99d7..6c4b1207e 100644
--- a/Makefile
+++ b/Makefile
@@ -35,8 +35,8 @@ LOCALINCLUDES= -I config -I tools -I scripts -I lib -I kernel -I library \
 	       -I contrib/extraction
 INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
 
-BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
-OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
+BYTEFLAGS=-rectypes $(INCLUDES) $(CAMLDEBUG)
+OPTFLAGS=-rectypes $(INCLUDES) $(CAMLTIMEPROF)
 OCAMLDEP=ocamldep
 DEPFLAGS=$(LOCALINCLUDES)
 
@@ -67,12 +67,12 @@ LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
     lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \
     lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo
 
-KERNEL=kernel/names.cmo kernel/univ.cmo kernel/term.cmo \
+KERNEL=kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \
        kernel/sign.cmo kernel/declarations.cmo \
        kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \
-       kernel/closure.cmo kernel/reduction.cmo kernel/inductive.cmo\
-       kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \
-       kernel/cooking.cmo kernel/safe_typing.cmo
+       kernel/closure.cmo kernel/reduction.cmo \
+       kernel/inductive.cmo kernel/type_errors.cmo kernel/typeops.cmo \
+       kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo
 
 LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \
 	library/lib.cmo library/goptions.cmo \
@@ -80,7 +80,7 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \
 	library/impargs.cmo library/indrec.cmo library/declare.cmo 
 
 PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \
-	  pretyping/retyping.cmo pretyping/tacred.cmo \
+	  pretyping/retyping.cmo pretyping/cbv.cmo pretyping/tacred.cmo \
 	  pretyping/pretype_errors.cmo pretyping/typing.cmo \
 	  pretyping/classops.cmo pretyping/recordops.cmo \
 	  pretyping/evarutil.cmo pretyping/evarconv.cmo \
@@ -155,11 +155,11 @@ COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP)
 world: $(COQBINARIES) states theories contrib tools
 
 $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX)
-	$(COQMKTOP) -opt $(OPTFLAGS) -o $@
+	$(COQMKTOP) -opt $(INCLUDES) $(CAMLDEBUG) -o $@
 	$(STRIP) $@
 
 $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO)
-	$(COQMKTOP) -top $(BYTEFLAGS) -o $@
+	$(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@
 
 # coqmktop 
 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 7b3b8f6f6..1cfbf965c 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -217,7 +217,7 @@ let _ =
 			 (constr_of amult)
 			 (constr_of aone)
 			 (constr_of azero)
-			 (mkXtra "not a term")
+			 mkImplicit
 			 (constr_of aeq)
 			 (constr_of t)
 			 (cset_of_comarg_list l)))
@@ -253,7 +253,7 @@ let _ =
 			 (constr_of amult)
 			 (constr_of aone)
 			 (constr_of azero)
-			 (mkXtra "not a term")
+			 mkImplicit
 			 (constr_of aeq)
 			 (constr_of t)
 			 ConstrSet.empty))
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 4d4b05d78..0f55481c3 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -485,8 +485,6 @@ let print_term inner_types l env csr =
 	   (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) (Array.of_list f) ) [<>]
        >]
 )
-   | T.IsXtra _ ->
-      Util.anomaly "Xtra node in a term!!!"
    | T.IsEvar _ ->
       Util.anomaly "Evar node in a term!!!"
   in
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 95c85866d..7cb08e06b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -82,7 +82,6 @@ let constr_display csr =
   | IsMeta n -> "Meta("^(string_of_int n)^")"
   | IsVar id -> "Var("^(string_of_id id)^")"
   | IsSort s -> "Sort("^(sort_display s)^")"
-  | IsXtra s -> "Xtra("^s^")"
   | IsCast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")"
   | IsProd (na,t,c) ->
       "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n"
@@ -145,7 +144,6 @@ let print_pure_constr csr =
   | IsMeta n -> print_string "Meta("; print_int n; print_string ")"
   | IsVar id -> print_string (string_of_id id)
   | IsSort s -> sort_display s
-  | IsXtra s -> print_string ("Xtra("^s^")")
   | IsCast (c,t) -> open_hovbox 1;
       print_string "("; (term_display c); print_cut();
       print_string "::"; (term_display t); print_string ")"; close_box()
diff --git a/kernel/closure.ml b/kernel/closure.ml
index d6e4589ca..7762b18bb 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -9,6 +9,8 @@ open Environ
 open Instantiate
 open Univ
 open Evd
+open Esubst
+
 
 let stats = ref false
 let share = ref true
@@ -29,6 +31,15 @@ let stop() =
 	   'sTR" zeta="; 'iNT !zeta; 'sTR" evar="; 'iNT !evar;
            'sTR" iota="; 'iNT !iota; 'sTR" prune="; 'iNT !prune; 'sTR"]" >]
 
+let with_stats c =
+  if !stats then begin
+    reset();
+    let r = Lazy.force c in
+    stop();
+    r
+  end else
+    Lazy.force c
+
 type evaluable_global_reference =
   | EvalVarRef of identifier
   | EvalConstRef of section_path
@@ -152,7 +163,7 @@ let red_set red = function
       let c = List.mem sp l in
       incr_cnt ((b & not c) or (c & not b)) delta
   | VAR id -> (* En attendant d'avoir des sp pour les Var *)
-      let (b,_,l) = red.r_const in
+     let (b,_,l) = red.r_const in
       let c = List.mem id l in
       incr_cnt ((b & not c) or (c & not b)) delta
   | ZETA -> incr_cnt red.r_zeta zeta
@@ -213,59 +224,6 @@ let red_under (md,r) rk =
     | WITHBACK -> true
     | _ -> red_set r rk
 
-(* (bounded) explicit substitutions of type 'a *)
-type 'a subs =
-  | 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 *)
-  | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
-
-(* operations of subs: collapses constructors when possible.
- * Needn't be recursive if we always use these functions
- *)
-
-let subs_cons(x,s) = CONS(x,s)
-
-let subs_liftn n = function
-  | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *)
-  | LIFT (p,lenv) -> LIFT (p+n, lenv)
-  | lenv -> LIFT (n,lenv)
-
-let subs_lift a = subs_liftn 1 a
-
-let subs_shft = function
-  | (0, s)            -> s
-  | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
-  | (n, s)            -> SHIFT (n,s)
-
-(* Expands de Bruijn k in the explicit substitution subs
- * lams accumulates de shifts to perform when retrieving the i-th value
- * the rules used are the following:
- *
- *    [id]k       --> k
- *    [S.t]1      --> t
- *    [S.t]k      --> [S](k-1)  if k > 1
- *    [^n o S] k  --> [^n]([S]k)
- *    [(%n S)] k  --> k         if k <= n
- *    [(%n S)] k  --> [^n]([S](k-n))
- *
- * 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,None)
-    | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l
-    | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s
-    | (_, ESID n) when k<=n -> Inr(lams+k,None)
-    | (_, 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
@@ -302,6 +260,8 @@ type ('a, 'b) infos = {
   i_vars : (identifier * constr) list;
   i_tab : ('a table_key, 'a) Hashtbl.t }
 
+let info_flags info = info.i_flags
+
 let ref_value_cache info ref =
   try  
     Some (Hashtbl.find info.i_tab ref)
@@ -344,383 +304,9 @@ let defined_rels flags env =
       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 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
- *          only when the abstraction is applied, and then we use the rule
- *                  ([S]([x:a]b) c) --> [S.c]b
- *          This corresponds to the usual strategy of weak reduction
- *  FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under
- *          the substitution S, and then applied to args. Here again,
- *          weak reduction.
- *  CONSTR(n,(sp,i),vars,args) is the n-th constructor of the i-th
- *          inductive type sp.
- *
- * Note that any term has not an equivalent in cbv_value: for example,
- * a product (x:A)B must be in normal form because only VAL may
- * represent it, and the argument of VAL is always in normal
- * form. This remark precludes coding a head reduction with these
- * functions. Anyway, does it make sense to head reduce with a
- * call-by-value strategy ?
- *)
-type cbv_value =
-  | VAL of int * constr
-  | LAM of name * constr * constr * cbv_value subs
-  | FIXP of fixpoint * cbv_value subs * cbv_value list
-  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
-  | CONSTR of int * inductive_path * cbv_value array * cbv_value list
-
-(* les vars pourraient etre des constr,
-   cela permet de retarder les lift: utile ?? *) 
-
-(* relocation of a value; used when a value stored in a context is expanded
- * in a larger context. e.g.  [%k (S.t)](k+1) --> [^k]t  (t is shifted of k)
- *)
-let rec shift_value n = function
-  | VAL (k,v) -> VAL ((k+n),v)
-  | LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s))
-  | FIXP (fix,s,args) ->
-      FIXP (fix,subs_shft (n,s), List.map (shift_value n) args)
-  | COFIXP (cofix,s,args) ->
-      COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args)
-  | CONSTR (i,spi,vars,args) ->
-      CONSTR (i, spi, Array.map (shift_value n) vars,
-              List.map (shift_value n) args)
-	
-
-(* Contracts a fixpoint: given a fixpoint and a substitution,
- * returns the corresponding fixpoint body, and the substitution in which
- * it should be evaluated: its first variables are the fixpoint bodies
- * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
- *    -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
- *)
-let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
-  let make_body j = FIXP(((reci,j),bodies), env, []) in
-  let n = Array.length bds in
-  let rec subst_bodies_from_i i subs =
-    if i=n then subs
-    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
-  in       
-  subst_bodies_from_i 0 env, bds.(i)
-
-let contract_cofixp env (i,(_,_,bds as bodies)) =
-  let make_body j = COFIXP((j,bodies), env, []) in
-  let n = Array.length bds in
-  let rec subst_bodies_from_i i subs =
-    if i=n then subs
-    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
-  in       
-  subst_bodies_from_i 0 env, bds.(i)
-
-
-(* type of terms with a hole. This hole can appear only under App or Case.
- *   TOP means the term is considered without context
- *   APP(l,stk) means the term is applied to l, and then we have the context st
- *      this corresponds to the application stack of the KAM.
- *      The members of l are values: we evaluate arguments before the function.
- *   CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk
- *      t is the type of the case and br are the branches, all of them under
- *      the subs S, pat is information on the patterns of the Case
- *      (Weak reduction: we propagate the sub only when the selected branch
- *      is determined)
- *
- * Important remark: the APPs should be collapsed:
- *    (APP (l,(APP ...))) forbidden
- *)
-
-type cbv_stack =
-  | TOP
-  | APP of cbv_value list * cbv_stack
-  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
-
-(* Adds an application list. Collapse APPs! *)
-let stack_app appl stack =
-  match (appl, stack) with
-    | ([], _)            -> stack
-    | (_, APP(args,stk)) -> APP(appl@args,stk)
-    | _                  -> APP(appl, stack)
-
-(* Tests if we are in a case (modulo some applications) *)
-let under_case_stack = function
-  | (CASE _ | APP(_,CASE _)) -> true
-  | _ -> false
-
-(* Tells if the reduction rk is allowed by flags under a given stack.
- * The stack is useful when flags is (SIMPL,r) because in that case,
- * we perform bdi-reduction under the Case, or r-reduction otherwise
- *)
-let red_allowed flags stack rk =
-  if under_case_stack stack then 
-    red_under flags rk
-  else 
-    red_top flags rk
-
-let red_allowed_ref flags stack = function
-  | FarRelBinding _ -> red_allowed flags stack DELTA
-  | VarBinding id -> red_allowed flags stack (VAR id)
-  | 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
- *)
-let strip_appl head stack =
-  match head with
-    | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack)
-    | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack)
-    | CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack)
-    | _ -> (head, stack)
-
-
-(* 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.
- *)
-let reduce_const_body redfun v stk =
-  if under_case_stack stk then strip_appl (redfun v) stk else strip_appl v stk
- 
-
-(* Tests if fixpoint reduction is possible. A reduction function is given as
-   argument *)
-let rec check_app_constr redfun = function
-  | ([], _) -> false
-  | ((CONSTR _)::_, 0) -> true
-  | (t::_, 0) -> (* TODO: partager ce calcul *)
-      (match redfun t with
-         | CONSTR _ -> true
-         | _ -> false)
-  | (_::l, n) -> check_app_constr redfun (l,(pred n))
-	
-let fixp_reducible redfun flgs ((reci,i),_) stk =
-  if red_allowed flgs stk IOTA then
-    match stk with               (* !!! for Acc_rec: reci.(i) = -2 *)
-      | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i))
-      | _ -> false
-  else 
-    false
-
-let cofixp_reducible redfun flgs _ stk =
-  if red_allowed flgs stk IOTA then
-    match stk with
-      | (CASE _ | APP(_,CASE _)) -> true
-      | _ -> false
-  else 
-    false
-
-let mindsp_nparams env (sp,i) =
-  let mib = lookup_mind sp env in
-  (Declarations.mind_nth_type_packet mib i).Declarations.mind_nparams
-
-(* The main recursive functions
- *
- * Go under applications and cases (pushed in the stack), expand head
- * constants or substitued de Bruijn, and try to make appear a
- * constructor, a lambda or a fixp in the head. If not, it is a value
- * and is completely computed here. The head redexes are NOT reduced:
- * the function returns the pair of a cbv_value and its stack.  *
- * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
- * argument is [].  Because we must put all the applied terms in the
- * stack. *)
-
-let rec norm_head info env t stack =
-  (* no reduction under binders *)
-  match kind_of_term t with
-  (* stack grows (remove casts) *)
-  | IsApp (head,args) -> (* Applied terms are normalized immediately;
-                        they could be computed when getting out of the stack *)
-      let nargs = Array.map (cbv_stack_term info TOP env) args in
-      norm_head info env head (stack_app (Array.to_list nargs) stack)
-  | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
-  | IsCast (ct,_) -> norm_head info env ct stack
-
-  (* constants, axioms
-   * the first pattern is CRUCIAL, n=0 happens very often:
-   * 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 env) v stack
-                | Inl (n,v) ->
-                    reduce_const_body
-                      (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-p) info env stack (FarRelBinding p))
-
-  | IsVar id -> norm_head_ref 0 info env stack (VarBinding id)
-
-  | IsConst (sp,vars) ->
-      let normt = (sp,Array.map (cbv_norm_term info env) vars) in
-      norm_head_ref 0 info env stack (ConstBinding normt)
-
-  | IsEvar ev -> norm_head_ref 0 info env stack (EvarBinding (ev,env))
-
-  | IsLetIn (x, b, t, c) ->
-      (* zeta means letin are contracted; delta without zeta means we *)
-      (* allow substitution but leave let's in place *)
-      let zeta = red_allowed info.i_flags stack ZETA in
-      let env' =
-	if zeta or red_allowed info.i_flags stack DELTA then 
-	  subs_cons (cbv_stack_term info TOP env b,env)
-	else
-	  subs_lift env in
-      if zeta then
-        norm_head info env' c stack
-      else
-	let normt =
-	  mkLetIn (x, cbv_norm_term info env b,
-		   cbv_norm_term info env t,
-		   cbv_norm_term info env' c) in
-	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
-
-  (* non-neutral cases *)
-  | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack)
-  | IsFix fix -> (FIXP(fix,env,[]), stack)
-  | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack)
-  | IsMutConstruct ((spi,i),vars) ->
-      (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack)
-
-  (* neutral cases *)
-  | (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) -> 
-      (VAL(0, mkProd (x, cbv_norm_term info env t,
-		      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 info normt), stack)
-  else (VAL(0,make_constr_ref k info normt), stack)
-
-and make_constr_ref n info = function
-  | FarRelBinding p -> mkRel (n+p)
-  | VarBinding id -> mkVar id
-  | EvarBinding ((ev,args),env) ->
-      mkEvar (ev,Array.map (cbv_norm_term info env) args)
-  | ConstBinding cst -> mkConst cst
-
-(* 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.
- * If so, recursive call to reach the real head normal form.  If not,
- * we build a value. 
- *)
-and cbv_stack_term info stack env t =
-  match norm_head info env t stack with
-    (* a lambda meets an application -> BETA *)
-    | (LAM (x,a,b,env), APP (arg::args, stk))
-      when red_allowed info.i_flags stk BETA ->
-        let subs = subs_cons (arg,env) in
-          cbv_stack_term info (stack_app args stk) subs b
-
-    (* a Fix applied enough -> IOTA *)
-    | (FIXP(fix,env,_), 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 env) info.i_flags cofix stk->
-        let (envf,redfix) = contract_cofixp env cofix in
-        cbv_stack_term info stk envf redfix
-
-    (* constructor in a Case -> IOTA
-       (use red_under because we know there is a Case) *)
-    | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,_,env,stk)))
-            when red_under info.i_flags IOTA ->
-              let nparams = mindsp_nparams info.i_env sp in
-              let real_args = snd (list_chop nparams args) in
-                cbv_stack_term info (stack_app real_args stk) env br.(n-1)
-         
-    (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
-    | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk))
-                  when red_under info.i_flags IOTA ->
-                    cbv_stack_term info stk env br.(n-1)
-
-    (* may be reduced later by application *)  
-    | (head, TOP) -> head
-    | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl) 
-    | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) 
-    | (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl)
-
-    (* definitely a value *)
-    | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
-
-
-(* if we are in SIMPL mode, maybe v isn't reduced enough *)
-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,env)) t
-    | _ -> v
-
-
-(* When we are sure t will never produce a redex with its stack, we
- * normalize (even under binders) the applied terms and we build the
- * final term
- *)
-and apply_stack info t = function
-  | TOP -> t
-  | APP (args,st) ->
-      apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st
-  | CASE (ty,br,ci,env,st) ->
-      apply_stack info
-        (mkMutCase (ci, cbv_norm_term info env ty, t,
-		    Array.map (cbv_norm_term info env) br))
-        st
-
-
-(* performs the reduction on a constr, and returns a constr *)
-and cbv_norm_term info env t =
-  (* reduction under binders *)
-  cbv_norm_value info (cbv_stack_term info TOP env t)
-
-(* reduction of a cbv_value to a constr *)
-and cbv_norm_value info = function (* reduction under binders *)
-  | VAL (n,v) -> lift n v
-  | LAM (x,a,b,env) ->
-      mkLambda (x, cbv_norm_term info env a,
-		cbv_norm_term info (subs_lift env) b)
-  | FIXP ((lij,(lty,lna,bds)),env,args) ->
-      applistc
-        (mkFix (lij,
-		(Array.map (cbv_norm_term info env) lty, lna, 
-		 Array.map (cbv_norm_term info 
-			      (subs_liftn (Array.length lty) env)) bds)))
-        (List.map (cbv_norm_value info) args)
-  | COFIXP ((j,(lty,lna,bds)),env,args) ->
-      applistc
-        (mkCoFix (j,
-		  (Array.map (cbv_norm_term info env) lty, lna, 
-		   Array.map (cbv_norm_term info 
-				(subs_liftn (Array.length lty) env)) bds)))
-        (List.map (cbv_norm_value info) args)
-  | CONSTR (n,spi,vars,args) ->
-      applistc
-        (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars))
-        (List.map (cbv_norm_value info) args)
-
-type 'a cbv_infos = (cbv_value, 'a) infos
-
-(* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env sigma =
+let create mk_cl flgs env sigma =
   { i_flags = flgs;
-    i_repr = (fun old_info s c -> cbv_stack_term old_info TOP s c);
+    i_repr = mk_cl;
     i_env = env;
     i_evc = sigma;
     i_rels = defined_rels flgs env;
@@ -728,633 +314,619 @@ let create_cbv_infos flgs env sigma =
     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 0) constr in
-    stop();
-    r
-  end else
-    cbv_norm_term infos (ESID 0) constr
-
+let infos_under infos = { infos with i_flags = flags_under infos.i_flags }
 
-(**** End of call by value ****)
 
 (**********************************************************************)
 (* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *) 
 
-type 'a stack =
-  | EmptyStack
-  | ConsStack of 'a array * int * 'a stack
+type 'a stack_member =
+  | Zapp of 'a array * int
+  | Zcase of case_info * 'a * 'a array
+  | Zfix of 'a * 'a stack
+  | Zshift of int
+  | Zupdate of 'a
 
-let empty_stack = EmptyStack
+and 'a stack = 'a stack_member list
 
-let decomp_stack = function
-  | EmptyStack -> None
-  | ConsStack (v, n, s) ->
-      Some (v.(n), (if n+1 = Array.length v then s else ConsStack (v, n+1, s)))
+let empty_stack = []
 
-let append_stack v s = if Array.length v = 0 then s else ConsStack (v,0,s)
+let append_stackn v p s = if Array.length v = p then s else Zapp(v,p)::s
+let append_stack v s = append_stackn v 0 s
 
-let rec app_stack = function
-  | f, EmptyStack -> f
-  | f, ConsStack (v, n, s) -> 
-      let args = if n=0 then v else Array.sub v n (Array.length v - n) in
-      app_stack (appvect (f, args), s)
+(* Collapse the shifts in the stack *)
+let zshift n s =
+  match (n,s) with
+      (0,_) -> s
+    | (_,Zshift(k)::s) -> Zshift(n+k)::s
+    | _ -> Zshift(n)::s
+
+let rec stack_args_size = function
+  | Zapp(v,n)::s -> Array.length v - n + stack_args_size s
+  | Zshift(_)::s -> stack_args_size s
+  | Zupdate(_)::s -> stack_args_size s
+  | _ -> 0
+
+(* Parameterization: check the a given reduction is allowed in the
+   context of the stack *)
+let can_red info stk r =
+  red_top info.i_flags r ||
+  (fst info.i_flags = SIMPL &&
+    List.exists (function (Zcase _|Zfix _) -> true | _ -> false) stk)
 
-let rec list_of_stack = function
-  | EmptyStack -> []
-  | ConsStack (v, n, s) ->
-      let args = if n=0 then v else  Array.sub v n (Array.length v - n) in
-      Array.fold_right (fun a l -> a::l) args (list_of_stack s)
 
+(* When used as an argument stack (only Zapp can appear) *)
+let decomp_stack = function
+  | Zapp(v,n)::s -> Some (v.(n), append_stackn v (n+1) s)
+  | [] -> None
+  | _ -> assert false
+let decomp_stackn = function
+  | Zapp(v,n)::s ->
+      ((if n = 0 then v else Array.sub v n (Array.length v - n)), s)
+  | _ -> assert false
 let array_of_stack s =
   let rec stackrec = function
-  | EmptyStack -> []
-  | ConsStack (v, n, s) ->
-      let args = if n=0 then v else  Array.sub v n (Array.length v - n) in
+  | [] -> []
+  | stk ->
+      let (args,s) = decomp_stackn stk in
       args :: (stackrec s)
   in Array.concat (stackrec s)
-
+let rec list_of_stack = function
+  | [] -> []
+  | stk ->
+      let (args,s) = decomp_stackn stk in
+      Array.fold_right (fun a l -> a::l) args (list_of_stack s)
+let rec app_stack = function
+  | f, [] -> f
+  | f, stk -> 
+      let (args,s) = decomp_stackn stk in
+      app_stack (appvect (f, args), s)
 let rec stack_assign s p c = match s with
-  | EmptyStack -> EmptyStack
-  | ConsStack (v, n, s) ->
+  | Zapp(v,n)::s ->
       let q = Array.length v - n in 
       if p >= q then
-	ConsStack (v, n, stack_assign s (p-q) c)
+	Zapp (v, n) :: stack_assign s (p-q) c
       else
 	let v' = Array.sub v n q in
 	v'.(p) <- c;
-	ConsStack (v', 0, s)
-
+	Zapp (v',0) :: s
+  | _ -> s
 let rec stack_tail p s =
   if p = 0 then s else
     match s with
-      | EmptyStack -> failwith "stack_shop"
-      | ConsStack (v, n, s) ->
+      | Zapp (v, n) :: s ->
 	  let q = Array.length v - n in
 	  if p >= q then stack_tail (p-q) s
-	  else ConsStack (v, n+p, s)
-
+	  else Zapp (v, n+p) :: s
+      | _ -> failwith "stack_tail"
 let rec stack_nth s p = match s with
-  | EmptyStack -> raise Not_found
-  | ConsStack (v, n, s) ->
+  | Zapp (v, n) :: s ->
       let q = Array.length v - n in
       if p >= q then stack_nth s (p-q)
       else v.(p+n)
+  | _ -> raise Not_found
 
-let rec stack_args_size = function
-  | EmptyStack -> 0
-  | ConsStack (v, n, s) -> Array.length v - n + stack_args_size s
 
+(**********************************************************************)
+(* Lazy reduction: the one used in kernel operations                  *)
 
-(* Version avec listes
-type stack = constr list
-
-let decomp_stack = function
-  | [] -> None
-  | v :: s -> Some (v,s)
-
-let append_stack v s = v@s
-*)
-
-(* Lazy reduction: the one used in kernel operations *)
-
-(* type of shared terms. freeze and frterm are mutually recursive.
+(* type of shared terms. fconstr and frterm are mutually recursive.
  * Clone of the Generic.term structure, but completely mutable, and
  * annotated with booleans (true when we noticed that the term is
  * normal and neutral) FLIFT is a delayed shift; allows sharing
- * between 2 lifted copies of a given term FFROZEN is a delayed
+ * between 2 lifted copies of a given term FCLOS is a delayed
  * substitution applied to a constr
  *)
+type red_state = Norm | Cstr | Whnf | Red
 
-type freeze = { 
-  mutable norm: bool; 
-  mutable term: frterm }
+type fconstr = { 
+  mutable norm: red_state; 
+  mutable term: fterm }
 
-and frterm =
+and fterm =
   | FRel of int
   | FAtom of constr
-  | FCast of freeze * freeze
-  | FFlex of frreference
-  | 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 frreference =
+  | FCast of fconstr * fconstr
+  | FFlex of freference
+  | FInd of inductive_path * fconstr array
+  | FConstruct of constructor_path * fconstr array
+  | FApp of fconstr * fconstr array
+  | FFix of (int array * int) * (fconstr array * name list * fconstr array)
+      * constr array * fconstr subs
+  | FCoFix of int * (fconstr array * name list * fconstr array)
+      * constr array * fconstr subs
+  | FCases of case_info * fconstr * fconstr * fconstr array
+  | FLambda of name * fconstr * fconstr * constr * fconstr subs
+  | FProd of name * fconstr * fconstr * constr * fconstr subs
+  | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs
+  | FLIFT of int * fconstr
+  | FCLOS of constr * fconstr subs
+
+and freference =
   (* only vars as args of FConst ... exploited for caching *)
-  | FConst of section_path * freeze array
-  | FEvar of (existential * freeze subs)
+  | FConst of section_path * fconstr array
+  | FEvar of (existential * fconstr subs)
   | FVar of identifier
   | FFarRel of int (* index in the rel_context part of _initial_ environment *)
 
-let reloc_flex r el = r
-
-let frterm_of v = v.term
-let is_val v = v.norm 
-
-(* Copies v2 in v1 and returns v1. The only side effect is here!  The
- * invariant of the reduction functions is that the interpretation of
- * v2 as a constr (e.g term_of_freeze below) is a reduct of the
- * interpretation of v1.
- *
- * The implementation without side effect, but losing sharing,
- * simply returns v2. *)
-
-let freeze_assign v1 v2 =
-  if !share then begin
-      v1.norm <- v2.norm;
-      v1.term <- v2.term;
-      v1
-  end else 
-    v2
-
-(* lift a freeze and yields a frterm.  No loss of sharing: the
- * resulting term takes advantage of any reduction performed in v.
- * i.e.: if (lift_frterm n v) yields w, reductions in w are reported
- * in w.term (yes: w.term, not only in w) The lifts are collapsed,
- * because we often insert lifts of 0. *)
-
-let rec lift_frterm n v =
-  match v.term with
-    | FLIFT (k,f) -> lift_frterm (k+n) f
-    | FAtom _ as ft -> { norm = true; term = ft }
-     	(* gene: closed terms *)
-    | _ -> { norm = v.norm; term = FLIFT (n,v) }
-
-
-(* lift a freeze, keep sharing, but spare records when possible (case
- * n=0 ... ) The difference with lift_frterm is that reductions in v
- * are reported only in w, and not necessarily in w.term (with
- * notations above). *)
-let lift_freeze n v =
-  match (n, v.term) with
-    | (0, _) | (_, FAtom _ ) -> v  (* identity lift or closed term *)
-    | _ -> lift_frterm n v
-
-
-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) *)
-(* traverse_term : freeze subs -> constr -> freeze *)
-let rec traverse_term env t =
+let fterm_of v = v.term
+let set_whnf v = if v.norm = Red then v.norm <- Whnf
+let set_cstr v = if v.norm = Red then v.norm <- Cstr
+let set_norm v = v.norm <- Norm
+let is_val v = v.norm = Norm
+
+(* Put an update mark in the stack, only if needed *)
+let zupdate m s =
+  if !share & m.norm = Red then Zupdate(m)::s else s
+
+(* Could issue a warning if no is still Red, pointing out that we loose
+   sharing. *)
+let update v1 (no,t) =
+  if !share then
+    (v1.norm <- no;
+     v1.term <- t;
+     v1)
+  else {norm=no;term=t}
+
+let rec lft_fconstr n ft =
+  match ft.term with
+    FLIFT(k,m) -> lft_fconstr (n+k) m
+  | _ -> {norm=ft.norm; term=FLIFT(n,ft)}
+let lift_fconstr k f =
+  if k=0 then f else lft_fconstr k f
+let lift_fconstr_vect k v =
+  if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
+
+let clos_rel e i =
+  match expand_rel i e with
+    | Inl(n,mt) -> lift_fconstr n mt
+    | Inr(k,None) -> {norm=Norm; term= FRel k}
+    | Inr(k,Some p) ->
+        lift_fconstr (k-p) {norm=Norm;term=FFlex(FFarRel p)}
+
+(* Optimization: do not enclose variables in a closure.
+   Makes variable access much faster *)
+let mk_clos e t =
   match kind_of_term t with
-    | IsRel i -> (match expand_rel i env with
-		  | Inl (lams,v) -> (lift_frterm lams v)
-		  | Inr (k,None) -> { norm = true; term = FRel k }
-		  | Inr (k,Some p) ->
-		      lift_frterm (k-p) 
-		      { norm = false; term = FFlex (FFarRel p) })
-    | IsVar x -> { norm = false; term = FFlex (FVar x) }
-    | IsMeta _ | IsSort _ | IsXtra _ ->  { norm = true; term = FAtom t }
+    | IsRel i -> clos_rel e i
+    | IsVar x -> { norm = Norm; term = FFlex (FVar x) }
+    | IsMeta _ | IsSort _ ->  { norm = Norm; term = FAtom t }
+    | (IsMutInd _|IsMutConstruct _|IsFix _|IsCoFix _
+      |IsLambda _|IsProd _) ->
+        {norm = Cstr; term = FCLOS(t,e)}
+    | (IsApp _|IsMutCase _|IsCast _|IsConst _|IsEvar _|IsLetIn _) ->
+        {norm = Red; term = FCLOS(t,e)}
+
+let mk_clos_vect env v = Array.map (mk_clos env) v
+
+(* Translate the head constructor of t from constr to fconstr. This
+   function is parameterized by the function to apply on the direct
+   subterms.
+   Could be used insted of mk_clos. *)
+let mk_clos_deep clos_fun env t =
+  match kind_of_term t with
+    | IsRel i -> clos_rel env i
+    | (IsVar _|IsMeta _ | IsSort _) -> mk_clos env t
     | IsCast (a,b) ->
-        { norm = false;
-          term = FCast (traverse_term env a, traverse_term env b)}
+        { norm = Red;
+          term = FCast (clos_fun env a, clos_fun env b)}
     | IsApp (f,v) ->
-        { norm = false;
-	  term = FApp (traverse_term env f, Array.map (traverse_term env) v) }
+        { norm = Red;
+	  term = FApp (clos_fun env f, Array.map (clos_fun env) v) }
     | IsMutInd (sp,v) ->
-        { norm = false; term = FInd (sp, Array.map (traverse_term env) v) }
+        { norm = Cstr; term = FInd (sp, Array.map (clos_fun env) v) }
     | IsMutConstruct (sp,v) ->
-        { norm = false; term = FConstruct (sp,Array.map (traverse_term env) v)}
+        { norm = Cstr; term = FConstruct (sp,Array.map (clos_fun env) v)}
     | IsConst (sp,v) ->
-        { norm = false;
-	  term = FFlex (FConst (sp,Array.map (traverse_term env) v)) }
+        { norm = Red;
+	  term = FFlex (FConst (sp,Array.map (clos_fun env) v)) }
     | IsEvar (_,v as ev) ->
-	assert (array_for_all (fun a -> isVar a or isRel a) v);
-        { norm = false;
+        { norm = Red;
 	  term = FFlex (FEvar (ev, env)) }
 
     | IsMutCase (ci,p,c,v) ->
-        { norm = false;
-	  term = FCases (ci, traverse_term env p, traverse_term env c,
-			 Array.map (traverse_term env) v) }
+        { norm = Red;
+	  term = FCases (ci, clos_fun env p, clos_fun env c,
+			 Array.map (clos_fun 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),
+        { norm = Cstr;
+	  term = FFix (op, (Array.map (clos_fun env) tys, lna,
+			    Array.map (clos_fun 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),
+        { norm = Cstr;
+	  term = FCoFix (op, (Array.map (clos_fun env) tys, lna,
+			      Array.map (clos_fun env') bds),
 			 bds, env) }
 
     | IsLambda (n,t,c) ->
-        { norm = false;
-	  term = FLambda (n, traverse_term env t,
-			  traverse_term (subs_lift env) c,
+        { norm = Cstr;
+	  term = FLambda (n, clos_fun env t,
+			  clos_fun (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,
+        { norm = Cstr;
+	  term = FProd (n, clos_fun env t, 
+			clos_fun (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,
+        { norm = Red;
+	  term = FLetIn (n, clos_fun env b, clos_fun env t,
+			 clos_fun (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 =
+(* The inverse of mk_clos_deep: move back to constr *)
+let rec to_constr constr_fun lfts v =
   match v.term with
-    | FRel i -> mkRel (reloc_rel i lfts)
-    | FFlex (FVar x) -> mkVar x
-    | FFlex (FFarRel p) -> mkRel (reloc_rel p 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 ((n,args), env)) ->
-	let f a = lift_term_of_freeze lfts (traverse_term env a) in
-	mkEvar (n, Array.map f args)
-    | 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) ->
-	mkApp (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)
-    | 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) ->
-        let unfv = freeze_assign v (traverse_term env t) in
-        lift_term_of_freeze lfts unfv
-
-
-(* This function defines the correspondance between constr and freeze *)
-let term_of_freeze v = lift_term_of_freeze ELID v
-let applist_of_freeze appl = Array.to_list (Array.map term_of_freeze appl)
-
-
-(* fstrong applies unfreeze_fun recursively on the (freeze) term and
- * yields a term.  Assumes that the unfreeze_fun never returns a
- * FFROZEN term. 
- *)
-let rec fstrong unfreeze_fun lfts v =
-  match (unfreeze_fun v).term with
-    | FRel i -> mkRel (reloc_rel i lfts)
-    | FFlex (FFarRel p) -> mkRel (reloc_rel p lfts)
-    | FFlex (FVar x) -> mkVar x
-    | FAtom c -> c
+    | FRel i -> IsRel (reloc_rel i lfts)
+    | FFlex (FFarRel p) -> IsRel (reloc_rel p lfts)
+    | FFlex (FVar x) -> IsVar x
+    | FAtom c ->
+        (match kind_of_term c with
+          | IsSort s -> IsSort s
+          | IsMeta m -> IsMeta m
+          | _ -> assert false)
     | FCast (a,b) ->
-        mkCast (fstrong unfreeze_fun lfts a, fstrong unfreeze_fun lfts b)
+        IsCast (constr_fun lfts a, constr_fun lfts b)
     | FFlex (FConst (op,ve)) ->
-	mkConst (op, Array.map (fstrong unfreeze_fun lfts) ve)
+	IsConst (op, Array.map (constr_fun lfts) ve)
     | FFlex (FEvar ((n,args),env)) ->
-	let f a = fstrong unfreeze_fun lfts (freeze env a) in
-	mkEvar (n, Array.map f args)
+	let f a = constr_fun lfts (mk_clos env a) in
+	IsEvar (n, Array.map f args)
     | FInd (op,ve) ->
-	mkMutInd (op, Array.map (fstrong unfreeze_fun lfts) ve)
+	IsMutInd (op, Array.map (constr_fun lfts) ve)
     | FConstruct (op,ve) -> 
-	mkMutConstruct (op, Array.map (fstrong unfreeze_fun lfts) ve)
+	IsMutConstruct (op, Array.map (constr_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)
+	IsMutCase (ci, constr_fun lfts p,
+		   constr_fun lfts c,
+		   Array.map (constr_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))
+	IsFix (op, (Array.map (constr_fun lfts) tys, lna,
+		    Array.map (constr_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))
+	IsCoFix (op, (Array.map (constr_fun lfts) tys, lna,
+		      Array.map (constr_fun lfts') bds))
     | FApp (f,ve) ->
-	mkApp (fstrong unfreeze_fun lfts f,
-		Array.map (fstrong unfreeze_fun lfts) ve)
+	IsApp (constr_fun lfts f,
+	       Array.map (constr_fun lfts) ve)
     | FLambda (n,t,c,_,_)   ->
-	mkLambda (n, fstrong unfreeze_fun lfts t,
-	      fstrong unfreeze_fun (el_lift lfts) c)
+	IsLambda (n, constr_fun lfts t,
+	             constr_fun (el_lift lfts) c)
     | FProd (n,t,c,_,_)   ->
-	mkProd (n, fstrong unfreeze_fun lfts t,
-	      fstrong unfreeze_fun (el_lift lfts) c)
+	IsProd (n, constr_fun lfts t,
+	           constr_fun (el_lift lfts) c)
     | 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"
-
-
-(* Build a freeze, which represents the substitution of arg in t
- * Used to constract a beta-redex:
- *           [^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
-  
+	IsLetIn (n, constr_fun lfts b,
+	      constr_fun lfts t,
+	      constr_fun (el_lift lfts) c)
+    | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
+    | FCLOS (t,env) ->
+        let fr = mk_clos_deep mk_clos env t in
+        let unfv = update v (fr.norm,fr.term) in
+        to_constr constr_fun lfts unfv
+
+(* This function defines the correspondance between constr and
+   fconstr. When we find a closure whose substitution is the identity,
+   then we directly return the constr to avoid possibly huge
+   reallocation. *)
+let term_of_fconstr =
+  let rec term_of_fconstr_lift lfts v =
+    match v.term with
+      | FCLOS(t,env) when is_subs_id env & is_lift_id lfts -> t
+      | _ -> mk_constr (to_constr term_of_fconstr_lift lfts v) in
+  term_of_fconstr_lift ELID
 
-(* Calculus of Constructions *)
 
-type fconstr = freeze
-
-(* 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
-    | FApp (f,args) ->
-        strip_frterm n f
-	  (append_stack (Array.map (lift_freeze n) args) stack)
-    | FCast (f,_) -> (strip_frterm n f stack)
-    | _ -> (n, v, stack)
-
-let strip_freeze v = strip_frterm 0 v empty_stack
 
+(* fstrong applies unfreeze_fun recursively on the (freeze) term and
+ * yields a term.  Assumes that the unfreeze_fun never returns a
+ * FCLOS term. 
+let rec fstrong unfreeze_fun lfts v =
+  to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v)
+*)
 
-(* Same as contract_fixp, but producing a freeze *)
+(* TODO: the norm flags are not handled properly *)
+let rec zip zfun m stk =
+  match stk with
+    | [] -> m
+    | Zapp(_)::_ ->
+        let (args,s) = decomp_stackn stk in
+        zip zfun {norm=m.norm; term=FApp(m, Array.map zfun args)} s
+    | Zcase(ci,p,br)::s ->
+        let t = FCases(ci, zfun p, m, Array.map zfun br) in
+        zip zfun {norm=m.norm; term=t} s
+    | Zfix(fx,par)::s ->
+        zip zfun fx (par @ append_stack [|m|] s)
+    | Zshift(n)::s ->
+        zip zfun (lift_fconstr n m) s
+    | Zupdate(rf)::s ->
+        zip zfun (update rf (m.norm,m.term)) s
+
+let fapp_stack (m,stk) = zip (fun x -> x) m stk
+
+(*********************************************************************)
+
+(* The assertions in the functions below are granted because they are
+   called only when m is a constructor, a cofix
+   (strip_update_shift_app), a fix (get_nth_arg) or an abstraction
+   (strip_update_shift, through get_arg). *)
+
+(* optimised for the case where there are no shifts... *)
+let strip_update_shift head stk =
+  assert (head.norm <> Red);
+  let rec strip_rec h depth = function
+    | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s
+    | Zupdate(m)::s ->
+        strip_rec (update m (h.norm,h.term)) depth s
+    | stk -> (depth,stk) in
+  strip_rec head 0 stk
+
+(* optimised for the case where there are no shifts... *)
+let strip_update_shift_app head stk =
+  assert (head.norm <> Red);
+  let rec strip_rec rstk h depth = function
+    | Zshift(k) as e :: s ->
+        strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
+    | (Zapp(_)::_) as stk ->
+        let (args,s) = decomp_stackn stk in
+        strip_rec (Zapp(args,0)::rstk)
+          {norm=h.norm;term=FApp(h,args)} depth s
+    | Zupdate(m)::s ->
+        strip_rec rstk (update m (h.norm,h.term)) depth s
+    | stk -> (depth,List.rev rstk, stk) in
+  strip_rec [] head 0 stk
+
+
+let rec get_nth_arg head n stk =
+  assert (head.norm <> Red);
+  let rec strip_rec rstk h depth n = function
+    | Zshift(k) as e :: s ->
+        strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
+    | Zapp(v, p)::s' ->
+        let q = Array.length v - p in
+        if n >= q
+        then
+          let v' = if p = 0 then v else Array.sub v p q in
+          strip_rec (Zapp(v',0)::rstk)
+            {norm=h.norm;term=FApp(h,v')} depth (n-q) s'
+        else
+          let rstk' =
+            if n = 0 then rstk else Zapp(Array.sub v p n,0)::rstk in
+          (Some (List.rev rstk', v.(p+n)), append_stackn v (p+n+1) s')
+    | Zupdate(m)::s ->
+        strip_rec rstk (update m (h.norm,h.term)) depth n s
+    | s -> (None, List.rev rstk @ s) in
+  strip_rec [] head 0 n stk
+
+(* Beta reduction: look for an applied argument in the stack.
+   Since the encountered update marks are removed, h must be a whnf *)
+let get_arg h stk =
+  let (depth,stk') = strip_update_shift h stk in
+  match stk' with
+      Zapp(v,p)::s -> (Some(depth,v.(p)), append_stackn v (p+1) s)
+    | _ -> (None, zshift depth stk')
+
+
+(* Iota reduction: extract the arguments to be passed to the Case
+   branches *)
+let rec reloc_rargs_rec depth stk =
+  match stk with
+      Zapp(_)::_ ->
+        let (args,s) = decomp_stackn stk in
+        Zapp(lift_fconstr_vect depth args,0) :: reloc_rargs_rec depth s
+    | Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s
+    | _ -> stk
+
+let reloc_rargs depth stk =
+  if depth = 0 then stk else reloc_rargs_rec depth stk
+
+let rec drop_parameters depth n stk =
+  match stk with
+      Zapp(v,p)::s ->
+        let q = Array.length v - p in
+        if n > q then drop_parameters depth (n-q) s
+        else if n = q then reloc_rargs depth s
+        else reloc_rargs depth (Zapp(v,p+n)::s)
+    | Zshift(k)::s -> drop_parameters (depth-k) n s
+    | [] -> assert (n=0); []
+    | _ -> assert false (* we know that n < stack_args_size(stk) *)
+
+
+(* Iota reduction: expansion of a fixpoint.
+ * Given a fixpoint and a substitution, returns the corresponding
+ * fixpoint body, and the substitution in which it should be
+ * evaluated: its first variables are the fixpoint bodies
+ *
+ * FCLOS(fix Fi {F0 := T0 .. Fn-1 := Tn-1}, S)
+ *    -> (S. FCLOS(F0,S) . ... . FCLOS(Fn-1,S), Ti)
+ *)
 (* does not deal with FLIFT *)
 let contract_fix_vect fix =
   let (thisbody, make_body, env, nfix) =
     match fix with
       | FFix ((reci,i),def,bds,env) ->
           (bds.(i),
-	   (fun j -> { norm = false; term = FFix ((reci,j),def,bds,env) }),
+	   (fun j -> { norm = Whnf; 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) }),
+	   (fun j -> { norm = Whnf; 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 env =
     if i = nfix then
-      freeze env thisbody
+      mk_clos env thisbody
     else
       subst_bodies_from_i (i+1) (subs_cons (make_body i, env))
   in       
   subst_bodies_from_i 0 env
 
 
-(* CoFix reductions are context dependent. Therefore, they cannot be shared. *)
-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 stack
-  | COFIX of int * int * (fconstr array * name list * fconstr array) *
-      fconstr stack * constr array * freeze subs
-  | IRREDUCTIBLE
-
-
-let constr_or_cofix env v =
-  let (lft_hd, head, appl) = strip_freeze v in
-  match head.term with
-    | FConstruct ((indsp,i),_) ->
-        let args = stack_tail (mindsp_nparams env indsp) appl in
-        CONSTRUCTOR (i, args)
-    | FCoFix (bnum, def, bds, env) -> COFIX (lft_hd,bnum,def,appl, bds, env)
-    | _ -> IRREDUCTIBLE
-
-let fix_reducible env unf_fun n stack =
-  if n < stack_args_size stack & n >= 0 (* e.g for Acc_rec: n = -2 *) then
-    let v = unf_fun (stack_nth stack n) in
-    match constr_or_cofix env v with
-      | CONSTRUCTOR _ -> true
-      | _ -> false
-  else 
-    false
-
-
-(* unfreeze computes the weak head normal form of v (according to the
- * flags in info) and updates the mutable term. 
- *)
-let rec unfreeze info v =
-  freeze_assign v (whnf_frterm info v)
-
-(* weak head normal form
- * Sharing info: the physical location of the ouput of this function
- * doesn't matter (only the values of its fields do). 
- *)
-and whnf_frterm info ft =
-  if ft.norm then begin
-    incr prune; ft
-  end else
-    match ft.term with
-      | FFROZEN (t,env) -> whnf_term info env t
-      | FLIFT (k,f) ->
-	  let uf = unfreeze info f in
-          { norm = uf.norm; term = FLIFT(k, uf) }
-      | FCast (f,_) -> whnf_frterm info f  (* remove outer casts *)
-      | FApp (f,appl) -> whnf_apply info f (append_stack appl empty_stack)
-      | FFlex (FConst (sp,vars)) ->
-	  let cst = (sp, Array.map term_of_freeze vars) in
-	  if red_under info.i_flags (CONST [sp]) then
-            (match ref_value_cache info (ConstBinding cst) with
-               | Some def ->
-                   let udef = unfreeze info def in
-                   lift_frterm 0 udef
-               | None ->
-		   { norm = true (* because only mkVar *); term = ft.term })
-	  else 
-	    ft
-      | FFlex (FEvar ((_,vars),_ as ev)) ->
-	  if red_under info.i_flags EVAR then
-            (match ref_value_cache info (EvarBinding ev) with
-               | Some def ->
-                   let udef = unfreeze info def in
-                   lift_frterm 0 udef
-               | None ->
-		   { norm = true (* because only mkVar/Rel *);term = ft.term })
-	  else 
-	    ft
-      | FFlex (FVar id) as t->
-	  if red_under info.i_flags (VAR id) 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 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 0 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) co in
-            (match constr_or_cofix info.i_env c with
-	       | 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 p red_cofix bl)
-               | _ ->
-		   { norm = is_val p & is_val co & array_for_all is_val bl;
-		     term = ft.term })
-          else 
-	    ft
-
-      | FLetIn (na,b,fd,fc,d,subs) ->
-          let c = unfreeze info b in
-	  if red_under info.i_flags ZETA then
-	    whnf_frterm info (contract_subst 0 d subs c)
-	  else
-	    { norm = false;
-	      term = FLetIn (na,c,fd,fc,d,subs) }
-
-      | FRel _ | FAtom _ -> { norm = true; term = ft.term }
-
-      | FFix _ | FCoFix _ | FInd _ | FConstruct _ | FLambda _ | FProd _ -> ft
-
-(* Weak head reduction: case of the application (head appl) *)
-and whnf_apply info head stack =
-  let head = unfreeze info head in
-  if stack = empty_stack then 
-    head
-  else
-    let (lft_hd,whd,lstack) = strip_frterm 0 head stack in
-    match whd.term with
-      | FLambda (_,_,_,t,subs) when red_under info.i_flags BETA ->
-	  (match decomp_stack lstack with
-	     | Some (c, stack') ->
-		 let vbody = contract_subst lft_hd t subs c in
-		 whnf_apply info vbody stack'
-	     | None -> assert false)
-      | FFix ((reci,bnum), _, _, _) as fx
-          when red_under info.i_flags IOTA
-            & fix_reducible info.i_env 
-	        (unfreeze (infos_under info)) reci.(bnum) lstack ->
-          let fix = contract_fix_vect fx in
-          whnf_apply info (lift_freeze lft_hd fix) lstack
-      | _ ->
-	  let appl = array_of_stack stack in
-	  { norm = (is_val head) & (array_for_all is_val 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 =
+(*********************************************************************)
+(* A machine that inspects the head of a term until it finds an
+   atom or a subterm that may produce a redex (abstraction,
+   constructor, cofix, letin, constant), or a neutral term (product,
+   inductive) *)
+let rec knh m stk =
+  if is_val m then (m,stk) else
+  match m.term with
+    | FLIFT(k,a) -> knh a (zshift k stk)
+    | FCLOS(t,e) -> knht e t (Zupdate(m)::stk)
+    | FApp(a,b) -> knh a (append_stack b (zupdate m stk))
+    | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk)
+    | FFix((ri,n),_,_,_) ->
+        (set_whnf m;
+         match get_nth_arg m ri.(n) stk with
+             (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk')
+           | (None, stk') -> (m,stk'))
+    | FCast(t,_) -> knh t stk
+(* cases where knh stops *)
+    | (FFlex _|FLetIn _) -> (m, stk)
+    | (FRel _|FAtom _) -> (set_norm m; (m, stk))
+    | (FLambda _|FConstruct _|FCoFix _|FInd _|FProd _) ->
+        (set_whnf m; (m, stk))
+
+(* The same for pure terms *)
+and knht e t stk =
   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
-		 (lift_frterm (n-k) { norm = false; term = FFlex(FFarRel 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 *)
-
-    | IsApp (f,ve) ->
-      	whnf_frterm info
-	  { norm = false; term = FApp (freeze env f, freeze_vect env ve)}
-    | IsConst (op,v) ->
-      	whnf_frterm info 
-	  { norm = false; term = FFlex (FConst (op, freeze_vect env v)) }
-    | IsEvar ev ->
-      	whnf_frterm info { norm = false; term = FFlex (FEvar (ev, env)) }
-    | 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 = FLambda (n, freeze env t, freeze (subs_lift env) c,
-		       c, env) }
-    | IsProd (n,t,c)   ->
-        { norm = false;
-	  term = FProd (n, freeze env t, freeze (subs_lift env) c,
-		       c, env) }
-
-    | 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) }
+    | IsApp(a,b) ->
+        knht e a (append_stack (mk_clos_vect e b) stk)
+    | IsMutCase(ci,p,t,br) ->
+        knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
+    | IsFix _ -> knh (mk_clos_deep mk_clos e t) stk
+    | IsCast(a,b) -> knht e a stk
+    | IsRel n -> knh (clos_rel e n) stk
+    | (IsLambda _|IsProd _|IsMutConstruct _|IsCoFix _|IsMutInd _|
+       IsLetIn _|IsConst _|IsVar _|IsEvar _|IsMeta _|IsSort _) ->
+        (mk_clos_deep mk_clos e t, stk)
+
+
+(***********************************************************************)
+
+(* Computes a normal form from the result of knh. *)
+let rec knr info m stk =
+  match m.term with
+  | FLambda(_,_,_,f,e) when can_red info stk BETA ->
+      (match get_arg m stk with
+          (Some(depth,arg),s) -> knit info (subs_shift_cons(depth,e,arg)) f s
+        | (None,s) -> (m,s))
+  | FFlex(FConst(sp,args)) when can_red info stk (CONST [sp]) ->
+      let cst = (sp, Array.map term_of_fconstr args) in
+      (match ref_value_cache info (ConstBinding cst) with
+          Some v -> kni info v stk
+        | None -> (set_norm m; (m,stk)))
+  | FFlex(FEvar ev) when can_red info stk EVAR ->
+(* In the case of evars, if it is not defined, then we do not set the
+   flag to Norm, because it may be instantiated later on *)
+      (match ref_value_cache info (EvarBinding ev) with
+          Some v -> kni info v stk
+        | None -> (m,stk))
+  | FFlex(FVar id) when can_red info stk (VAR id) ->
+      (match ref_value_cache info (VarBinding id) with
+          Some v -> kni info v stk
+        | None -> (set_norm m; (m,stk)))
+  | FFlex(FFarRel k) when can_red info stk DELTA ->
+      (match ref_value_cache info (FarRelBinding k) with
+          Some v -> kni info v stk
+        | None -> (set_norm m; (m,stk)))
+  | FConstruct((sp,c),args) when can_red info stk IOTA ->
+      (match strip_update_shift_app m stk with
+          (depth, args, Zcase((cn,_),_,br)::s) ->
+            let npar = stack_args_size args - cn.(c-1) in
+            assert (npar>=0);
+            let rargs = drop_parameters depth npar args in
+            kni info br.(c-1) (rargs@s)
+        | (_, cargs, Zfix(fx,par)::s) ->
+            let rarg = fapp_stack(m,cargs) in
+            let stk' = par @ append_stack [|rarg|] s in
+            let efx = contract_fix_vect fx.term in
+            kni info efx stk'
+        | (_,args,s) -> (m,args@s))
+  | FCoFix _ when can_red info stk IOTA ->
+      (match strip_update_shift_app m stk with
+          (_, args, (Zcase((cn,_),_,br)::s as stk')) ->
+            let efx = contract_fix_vect m.term in
+            kni info efx (args@s)
+        | (_,args,s) -> (m,args@s))
+  | FLetIn (_,v,_,_,bd,e) when can_red info stk ZETA ->
+      knit info (subs_cons(v,e)) bd stk
+  | _ -> (m,stk)
+
+(* Computes the normal form of a term *)
+and kni info m stk =
+  let (hm,s) = knh m stk in
+  knr info hm s
+and knit info e t stk =
+  let (ht,s) = knht e t stk in
+  knr info ht s
+
+let kh info v stk = fapp_stack(kni info v stk)
+
+(***********************************************************************)
+
+(* Computes the strong normal form of a term.
+   1- Calls kni
+   2- tries to rebuild the term. If a closure still has to be computed,
+      calls itself recursively. *)
+let rec kl info m =
+  let (nm,s) = kni info m [] in
+  down_or_up info nm s
+
+(* no redex: go up for atoms and already normalized terms, go down
+   otherwise. *) 
+and down_or_up info m stk =
+  let nm =
+    if is_val m then (incr prune; m) else 
+      let nt =
+      match m.term with
+        | FLambda(na,ty,bd,f,e) ->
+            FLambda(na, kl info ty, kl info bd, f, e)
+        | FLetIn(na,a,b,c,f,e) ->
+            FLetIn(na, kl info a, kl info b, kl info c, f, e)
+        | FProd(na,dom,rng,f,e) ->
+            FProd(na, kl info dom, kl info rng, f, e)
+        | FInd(ind,args) ->
+            FInd(ind, Array.map (kl info) args)
+        | FConstruct(c,args) ->
+            FConstruct(c, Array.map (kl info) args)
+        | FCoFix(n,(ftys,na,fbds),bds,e) ->
+            FCoFix(n,(Array.map (kl info) ftys, na,
+                      Array.map (kl info) fbds),bds,e)
+        | FFlex(FConst(sp,args)) ->
+            FFlex(FConst(sp, Array.map (kl info) args))
+        | FFlex(FEvar((i,args),e)) ->
+            FFlex(FEvar((i,args),e))
+        | t -> t in
+      {norm=Norm;term=nt} in
+(* Precondition: m.norm = Norm *)
+  zip (kl info) nm stk
+
+
+(* Initialization and then normalization *)
+
+(* weak reduction *)
+let whd_val info v =
+  with_stats (lazy (term_of_fconstr (kh info v [])))
 
-(* parameterized norm *)
+(* strong reduction *)
 let norm_val info v =
-  if !stats then begin
-    reset();
-    let r = fstrong (unfreeze info) ELID v in
-    stop();
-    r
-  end else
-    fstrong (unfreeze info) ELID v
+  with_stats (lazy (term_of_fconstr (kl info v)))
 
-let whd_val info v =
-  let uv = unfreeze info v in
-  term_of_freeze uv
+let inject = mk_clos (ESID 0)
+
+(* cache of constants: the body is computed only when needed. *)
+type 'a clos_infos = (fconstr, 'a) infos
 
-let inject = freeze (ESID 0)
+let create_clos_infos flgs env sigma =
+  create (fun _ -> mk_clos) flgs env sigma
 
-let search_frozen_value info = function
+let unfold_reference info = function
   | FConst (op,v) -> 
       let cst = (op, Array.map (norm_val info) v) in
       ref_value_cache info (ConstBinding cst)
@@ -1362,26 +934,22 @@ let search_frozen_value info = function
   | FVar id -> ref_value_cache info (VarBinding id)
   | FFarRel p -> ref_value_cache info (FarRelBinding p)
 
-(* cache of constants: the body is computed only when needed. *)
-type 'a clos_infos = (fconstr, 'a) infos
-
+(* Head normal form. *)
 
-let create_clos_infos flgs env sigma =
-  { i_flags = flgs;
-    i_repr = (fun old_info s c -> freeze s c);
-    i_env = env;
-    i_evc = sigma;
-    i_rels = defined_rels flgs env;
-    i_vars = defined_vars flgs env;
-    i_tab = Hashtbl.create 17 }
+(* TODO: optimise *)
+let rec strip_applstack k acc m =
+  match m.term with
+      FApp(a,b) ->
+        strip_applstack k (append_stack (lift_fconstr_vect k b) acc) a
+    | FLIFT(n,a) ->
+        strip_applstack (k+n) acc a
+    | FCLOS _ -> assert false
+    | _ -> (k,m,acc)
 
-let clos_infos_env infos = infos.i_env
 
-(* Head normal form. *)
 let fhnf info v =
-  let uv = unfreeze info v in
-  strip_freeze uv
+  strip_applstack 0 [] (kh info v [])
 
-let fhnf_apply infos k head appl =
-  let v = whnf_apply infos (lift_freeze k head) appl in
-  strip_freeze v
+let fhnf_apply info k head appl =
+  let stk = zshift k appl in
+  strip_applstack 0 [] (kh info head stk)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index e3476db21..b4001f077 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -7,12 +7,15 @@ open Names
 open Term
 open Evd
 open Environ
+open Esubst
 (*i*)
 
 (* Flags for profiling reductions. *)
 val stats : bool ref
 val share : bool ref
 
+val with_stats: 'a Lazy.t -> 'a
+
 type evaluable_global_reference =
   | EvalVarRef of identifier
   | EvalConstRef of section_path
@@ -75,16 +78,23 @@ val betadeltaiota : flags
 val hnf_flags : flags
 val unfold_flags : evaluable_global_reference -> flags
 
-(*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 of int
-  | CONS of 'a * 'a subs
-  | SHIFT of int * 'a subs
-  | LIFT of int * 'a subs
+(***********************************************************************)
+
+type 'a table_key =
+  | ConstBinding of constant
+  | EvarBinding of (existential * 'a subs)
+  | VarBinding of identifier
+  | FarRelBinding of int
 
+type ('a,'b) infos
+val ref_value_cache: ('a,'b) infos -> 'a table_key -> 'a option
+val info_flags: ('a,'b) infos -> flags
+val infos_under: ('a,'b) infos -> ('a,'b) infos
+val create:
+  (('a,'b) infos -> 'a subs -> constr -> 'a) ->
+  flags -> env -> 'b evar_map -> ('a,'b) infos
+
+(***********************************************************************)
 (*s A [stack] is a context of arguments, arguments are pushed by
    [append_stack] one array at a time but popped with [decomp_stack]
    one by one *)
@@ -92,6 +102,7 @@ type 'a subs =
 type 'a stack
 val empty_stack : 'a stack
 val append_stack : 'a array -> 'a stack -> 'a stack
+
 val decomp_stack : 'a stack -> ('a * 'a stack) option
 val list_of_stack : 'a stack -> 'a list
 val array_of_stack : 'a stack -> 'a array
@@ -102,27 +113,20 @@ val stack_tail : int -> 'a stack -> 'a stack
 val stack_nth : 'a stack -> int -> 'a
 
 (***********************************************************************)
-(*s Call-by-value reduction *)
-
-(* Entry point for cbv normalization of a constr *)
-type 'a cbv_infos
-val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
-val cbv_norm : 'a cbv_infos -> constr -> constr
-
 (*s Lazy reduction. *)
 
 (* [fconstr] is the type of frozen constr *)
 
 type fconstr
 
-(* [fconstr] can be accessed by using the function [frterm_of] and by
-   matching on type [frterm] *)
+(* [fconstr] can be accessed by using the function [fterm_of] and by
+   matching on type [fterm] *)
 
-type frterm =
+type fterm =
   | FRel of int
   | FAtom of constr
   | FCast of fconstr * fconstr
-  | FFlex of frreference
+  | FFlex of freference
   | FInd of inductive_path * fconstr array
   | FConstruct of constructor_path * fconstr array
   | FApp of fconstr * fconstr array
@@ -135,26 +139,26 @@ type frterm =
   | FProd of name * fconstr * fconstr * constr * fconstr subs
   | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs
   | FLIFT of int * fconstr
-  | FFROZEN of constr * fconstr subs
+  | FCLOS of constr * fconstr subs
 
-and frreference =
+and freference =
   | FConst of section_path * fconstr array
   | FEvar of (existential * fconstr subs)
   | FVar of identifier
   | FFarRel of int
 
-val frterm_of : fconstr -> frterm
 
 (* To lazy reduce a constr, create a ['a clos_infos] with
    [create_cbv_infos], inject the term to reduce with [inject]; then use
    a reduction function *)
 
+val inject : constr -> fconstr
+val fterm_of : fconstr -> fterm
+val term_of_fconstr : fconstr -> constr
+
 (* 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
-
-val inject : constr -> fconstr
 
 (* Reduction function *)
 
@@ -164,92 +168,35 @@ val norm_val : 'a clos_infos -> fconstr -> constr
 (* [whd_val] is for weak head normalization *)
 val whd_val : 'a clos_infos -> fconstr -> constr
 
+(* Conversion auxiliary functions to do step by step normalisation *)
+
 (* [fhnf] and [fnf_apply] are for weak head normalization but staying
-   in [fcontr] world to perform step by step weak head normalization *)
+   in [fconstr] world to perform step by step weak head normalization *)
 
 val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr stack
 val fhnf_apply : 'a clos_infos ->
   int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack
 
-(* [search_frozen_value] unfolds references in a [fconstr] *)
-val search_frozen_value : 'a clos_infos -> frreference -> fconstr option
-
-
-(*i This is for cbv debug *)
-type cbv_value =
-  | VAL of int * constr
-  | LAM of name * constr * constr * cbv_value subs
-  | FIXP of fixpoint * cbv_value subs * cbv_value list
-  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
-  | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
-
-val shift_value : int -> cbv_value -> cbv_value
-
-type cbv_stack =
-  | TOP
-  | APP of cbv_value list * cbv_stack
-  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
-
-val stack_app : cbv_value list -> cbv_stack -> cbv_stack
-val under_case_stack : cbv_stack -> bool
-val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
-
-val red_allowed : flags -> cbv_stack -> red_kind -> bool
-val reduce_const_body :
-  (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack
-
-(* recursive functions... *)
-val cbv_stack_term : 'a cbv_infos ->
-  cbv_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 subs -> cbv_value -> cbv_value
-val norm_head : 'a cbv_infos ->
-  cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack
-val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr
-val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
-(* End of cbv debug section i*)
+(* [unfold_reference] unfolds references in a [fconstr] *)
+val unfold_reference : 'a clos_infos -> freference -> fconstr option
 
+(***********************************************************************)
 (*i This is for lazy debug *)
-type freeze = fconstr
-val is_val : freeze -> bool
 
-val lift_frterm : int -> freeze -> freeze
-val lift_freeze : int -> freeze -> freeze
+val lift_fconstr : int -> fconstr -> fconstr
+val lift_fconstr_vect : int -> fconstr array -> fconstr array
 
-val freeze : freeze subs -> constr -> freeze
-val freeze_vect : freeze subs -> constr array -> freeze array
-val freeze_list : freeze subs -> constr list -> freeze list
+val mk_clos : fconstr subs -> constr -> fconstr
+val mk_clos_vect : fconstr subs -> constr array -> fconstr array
+val mk_clos_deep :
+  (fconstr subs -> constr -> fconstr) ->
+   fconstr subs -> constr -> fconstr
 
-val traverse_term : freeze subs -> constr -> freeze
-val lift_term_of_freeze : lift_spec -> freeze -> constr
+val knr: 'a clos_infos -> fconstr -> fconstr stack ->
+  fconstr * fconstr stack
+val kl: 'a clos_infos -> fconstr -> fconstr
 
-(* Back to constr *)
-val fstrong : (freeze -> freeze) -> lift_spec -> freeze -> constr
-val term_of_freeze : freeze -> constr
-val applist_of_freeze : freeze array -> constr list
-
-(* contract a substitution *)
-val contract_subst : int -> constr -> freeze subs -> freeze -> freeze
-
-val strip_frterm :
-  int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack
-val strip_freeze : fconstr -> int * fconstr * fconstr stack
-
-(* Auxiliary functions for (co)fixpoint reduction *)
-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 stack
-  | COFIX of int * int * (fconstr array * name list * fconstr array) *
-      fconstr stack * constr array * freeze subs
-  | IRREDUCTIBLE
-
-(* recursive functions... *)
-val unfreeze : 'a clos_infos -> fconstr -> fconstr
-val whnf_frterm : 'a clos_infos -> fconstr -> fconstr
-val whnf_term : 'a clos_infos -> fconstr subs -> constr -> fconstr
-val whnf_apply : 'a clos_infos -> fconstr -> fconstr stack -> fconstr
+val to_constr :
+  (lift -> fconstr -> 'a) -> lift -> fconstr -> ('a,'a) kind_of_term
 
 (* End of cbn debug section i*)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6bec01ecd..f88860935 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -255,7 +255,7 @@ let hdchar env c =
     | IsCoFix (i,(_,ln,_)) -> 
 	let id = match List.nth ln i with Name id -> id | _ -> assert false in
 	lowercase_first_char id
-    | IsMeta _|IsXtra _|IsEvar _|IsMutCase (_, _, _, _) -> "y"
+    | IsMeta _|IsEvar _|IsMutCase (_, _, _, _) -> "y"
   in 
   hdrec 0 c
 
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
new file mode 100644
index 000000000..0ab021e4c
--- /dev/null
+++ b/kernel/esubst.ml
@@ -0,0 +1,111 @@
+
+(* $Id$ *)
+
+open Util
+
+(*********************)
+(*      Lifting      *)
+(*********************)
+
+(* Explicit lifts and basic operations *)
+type lift =
+  | ELID
+  | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
+  | ELLFT of int * lift  (* ELLFT(n,l)  == apply l to de Bruijn > n *)
+                         (*                 i.e under n binders *)
+
+(* compose a relocation of magnitude n *)
+let rec el_shft n = function
+  | ELSHFT(el,k) -> el_shft (k+n) el
+  | el -> if n = 0 then el else ELSHFT(el,n)
+
+
+(* cross n binders *)
+let rec el_liftn n = function
+  | ELID -> ELID
+  | ELLFT(k,el) -> el_liftn (n+k) el
+  | el -> if n=0 then el else ELLFT(n, el)
+
+let el_lift el = el_liftn 1 el
+
+(* relocation of de Bruijn n in an explicit lift *)
+let rec reloc_rel n = function
+  | ELID -> n
+  | ELLFT(k,el) ->
+      if n <= k then n else (reloc_rel (n-k) el) + k
+  | ELSHFT(el,k) -> (reloc_rel (n+k) el)
+
+let rec is_lift_id = function
+  | ELID -> true
+  | ELSHFT(e,n) -> n=0 & is_lift_id e
+  | ELLFT (_,e) -> is_lift_id e
+
+(*********************)
+(*  Substitutions    *)
+(*********************)
+
+(* (bounded) explicit substitutions of type 'a *)
+type 'a subs =
+  | 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 *)
+  | LIFT of int * 'a subs  (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
+
+(* operations of subs: collapses constructors when possible.
+ * Needn't be recursive if we always use these functions
+ *)
+
+let subs_cons(x,s) = CONS(x,s)
+
+let subs_liftn n = function
+  | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *)
+  | LIFT (p,lenv) -> LIFT (p+n, lenv)
+  | lenv -> LIFT (n,lenv)
+
+let subs_lift a = subs_liftn 1 a
+
+let subs_shft = function
+  | (0, s)            -> s
+  | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
+  | (n, s)            -> SHIFT (n,s)
+
+let subs_shift_cons = function
+  (0, s, t) -> CONS(t,s)
+| (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1))
+| (k, s, t) -> CONS(t,SHIFT(k, s));;
+
+(* Tests whether a substitution is extensionnaly equal to the identity *)
+let rec is_subs_id = function
+    ESID _ -> true
+  | LIFT(_,s) -> is_subs_id s
+  | SHIFT(0,s) -> is_subs_id s
+  | _ -> false
+
+(* Expands de Bruijn k in the explicit substitution subs
+ * lams accumulates de shifts to perform when retrieving the i-th value
+ * the rules used are the following:
+ *
+ *    [id]k       --> k
+ *    [S.t]1      --> t
+ *    [S.t]k      --> [S](k-1)  if k > 1
+ *    [^n o S] k  --> [^n]([S]k)
+ *    [(%n S)] k  --> k         if k <= n
+ *    [(%n S)] k  --> [^n]([S](k-n))
+ *
+ * the result is (Inr (k+lams,p)) when the variable is just relocated
+ * where p is None if the variable points inside 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,None)
+    | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l
+    | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s
+    | (_, ESID n) when k<=n -> Inr(lams+k,None)
+    | (_, ESID n) -> Inr(lams+k,Some (k-n))
+
+let expand_rel k subs = exp_rel 0 k subs
+
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
new file mode 100644
index 000000000..ea5df0a28
--- /dev/null
+++ b/kernel/esubst.mli
@@ -0,0 +1,34 @@
+
+(* $Id$ *)
+
+(*s Compact representation of explicit relocations. \\
+   [ELSHFT(l,n)] == lift of [n], then apply [lift l].
+   [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+type lift =
+  | ELID
+  | ELSHFT of lift * int
+  | ELLFT of int * lift
+
+val el_shft : int -> lift -> lift
+val el_liftn : int -> lift -> lift
+val el_lift : lift -> lift
+val reloc_rel : int -> lift -> int
+val is_lift_id : lift -> bool
+
+(*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 of int
+  | CONS of 'a * 'a subs
+  | SHIFT of int * 'a subs
+  | LIFT of int * 'a subs
+
+val subs_cons: 'a * 'a subs -> 'a subs
+val subs_shft: int * 'a subs -> 'a subs
+val subs_lift: 'a subs -> 'a subs
+val subs_liftn: int -> 'a subs -> 'a subs
+val subs_shift_cons: int * 'a subs * 'a -> 'a subs
+val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
+val is_subs_id: 'a subs -> bool
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 620f31eaa..a5920f870 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -345,14 +345,6 @@ let build_branch_type env dep p cs =
 
 (* [Rel (n+m);...;Rel(n+1)] *)
 
-let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (mkRel(n+p)::l) (p+1)
-  in 
-  reln [] 1
-
 let extended_rel_list n hyps =
   let rec reln l p = function
     | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e7504bf16..4980b9196 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -116,11 +116,6 @@ val build_dependent_constructor : constructor_summary -> constr
    the constructor argument of a dependent predicate in a cases branch *)
 val build_dependent_inductive : inductive_family -> constr
 
-(*s [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
-(* (this is iota operator in C. Paulin habilitation thesis) *)
-val rel_vect : int -> int -> constr array
-val rel_list : int -> int -> constr list
-
 (*s [extended_rel_vect n hyps] and [extended_rel_list n hyps]
     generalizes [rel_vect] when local definitions may occur in parameters *)
 val extended_rel_vect : int -> rel_context -> constr array
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 21ab932eb..7c244c280 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -11,6 +11,7 @@ open Declarations
 open Environ
 open Instantiate
 open Closure
+open Esubst
 
 exception Elimconst
 
@@ -78,7 +79,6 @@ 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)
 
@@ -710,7 +710,7 @@ and eqappr cv_pb infos appr1 appr2 =
   and (lft2,(n2,hd2,v2)) = appr2 in
   let el1 = el_shft n1 lft1
   and el2 = el_shft n2 lft2 in
-  match (frterm_of hd1, frterm_of hd2) with
+  match (fterm_of hd1, fterm_of hd2) with
     (* case of leaves *)
     | (FAtom a1, FAtom a2) ->
 	(match kind_of_term a1, kind_of_term a2 with
@@ -722,10 +722,6 @@ and eqappr cv_pb infos appr1 appr2 =
                bool_and_convert (n=m) 
 		 (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2)
 		    v1 v2)
-	   | IsXtra s1, IsXtra s2 ->
-               bool_and_convert (s1=s2)
-		 (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2)
-		    v1 v2)
 	   | _ -> fun _ -> raise NotConvertible)
 
     (* 2 index known to be bound to no constant *)
@@ -742,22 +738,22 @@ and eqappr cv_pb infos appr1 appr2 =
 	     (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))
           (* else expand the second occurrence (arbitrary heuristic) *)
           (fun u ->
-	     match search_frozen_value infos fl2 with
+	     match unfold_reference infos fl2 with
              | Some def2 -> 
 		 eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) u
-             | None -> (match search_frozen_value infos fl1 with
+             | None -> (match unfold_reference infos fl1 with
                           | Some def1 -> eqappr cv_pb infos
 				(lft1, fhnf_apply infos n1 def1 v1) appr2 u
 			  | None -> raise NotConvertible))
 
     (* only one constant, existential, defined var or defined rel *)
     | (FFlex fl1, _)      ->
-        (match search_frozen_value infos fl1 with
+        (match unfold_reference infos fl1 with
            | Some def1 -> 
 	       eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2
            | None -> fun _ -> raise NotConvertible)
     | (_, FFlex fl2)      ->
-        (match search_frozen_value infos fl2 with
+        (match unfold_reference infos fl2 with
            | Some def2 -> 
 	       eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2)
            | None -> fun _ -> raise NotConvertible)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f98ee5bdd..eecde292a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -138,8 +138,6 @@ let rec execute mf env cstr =
 	let (j, cst0) = cast_rel env Evd.empty cj tj in
 	(j, Constraint.union cst cst0)
 	  
-    | IsXtra _ -> anomaly "Safe_typing: found an Extra"
-	  
 and execute_fix mf env lar lfi vdef =
   let (larj,cst1) = execute_array mf env lar in
   let lara = Array.map (assumption_of_judgment env Evd.empty) larj in
diff --git a/kernel/term.ml b/kernel/term.ml
index d75bea008..533f013e4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -7,6 +7,7 @@ open Util
 open Pp
 open Names
 open Univ
+open Esubst
 
 (* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
 
@@ -70,13 +71,12 @@ type kind_of_term =
   | IsRel          of int
   | IsMeta         of int
   | IsVar          of identifier
-  | IsXtra         of string
   | IsSort         of sorts
   | IsCast         of constr * constr
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsLetIn        of name * constr * constr * constr
-  | IsApp         of constr * constr array
+  | IsApp          of constr * constr array
   | IsEvar         of existential
   | IsConst        of constant
   | IsMutInd       of inductive
@@ -88,7 +88,6 @@ type kind_of_term =
 val mkRel : int -> constr
 val mkMeta : int -> constr
 val mkVar : identifier -> constr
-val mkXtra : string -> constr
 val mkSort : sorts -> constr
 val mkCast : constr * constr -> constr
 val mkProd : name * constr * constr -> constr
@@ -119,34 +118,54 @@ module Internal : InternalSig =
 struct
 *)
 
-type constr = kind_of_term
-
-and existential = existential_key * constr array
-and constant = constant_path * constr array
-and constructor = constructor_path * constr array
-and inductive = inductive_path * constr array
-and rec_declaration = constr array * name list * constr array
-and fixpoint = (int array * int) * rec_declaration
-and cofixpoint = int * rec_declaration
-
-and kind_of_term =
+module Polymorph =
+struct
+(* [constr array] is an instance matching definitional [named_context] in
+   the same order (i.e. last argument first) *)
+type 'constr existential = existential_key * 'constr array
+type 'constr constant = constant_path * 'constr array
+type 'constr constructor = constructor_path * 'constr array
+type 'constr inductive = inductive_path * 'constr array
+type ('constr, 'types) rec_declaration =
+    'types array * name list * 'constr array
+type ('constr, 'types) fixpoint =
+    (int array * int) * ('constr, 'types) rec_declaration
+type ('constr, 'types) cofixpoint =
+    int * ('constr, 'types) rec_declaration
+
+(* [IsVar] is used for named variables and [IsRel] for variables as
+   de Bruijn indices. *)
+
+end 
+open Polymorph
+
+type ('constr, 'types) kind_of_term =
   | IsRel          of int
   | IsMeta         of int
   | IsVar          of identifier
-  | IsXtra         of string
   | IsSort         of sorts
-  | IsCast         of constr * constr
-  | IsProd         of name * constr * constr
-  | IsLambda       of name * constr * constr
-  | IsLetIn        of name * constr * constr * constr
-  | IsApp         of constr * constr array
-  | IsEvar         of existential
-  | IsConst        of constant
-  | IsMutInd       of inductive
-  | IsMutConstruct of constructor
-  | IsMutCase      of case_info * constr * constr * constr array
-  | IsFix          of fixpoint
-  | IsCoFix        of cofixpoint
+  | IsCast         of 'constr * 'constr
+  | IsProd         of name * 'types * 'constr 
+  | IsLambda       of name * 'types * 'constr
+  | IsLetIn        of name * 'constr * 'types * 'constr
+  | IsApp          of 'constr * 'constr array
+  | IsEvar         of 'constr existential
+  | IsConst        of 'constr constant
+  | IsMutInd       of 'constr inductive
+  | IsMutConstruct of 'constr constructor
+  | IsMutCase      of case_info * 'constr * 'constr * 'constr array
+  | IsFix          of ('constr, 'types) fixpoint
+  | IsCoFix        of ('constr, 'types) cofixpoint
+
+type constr = (constr,constr) kind_of_term
+
+type existential = existential_key * constr array
+type constant = constant_path * constr array
+type constructor = constructor_path * constr array
+type inductive = inductive_path * constr array
+type rec_declaration = constr array * name list * constr array
+type fixpoint = (int array * int) * rec_declaration
+type cofixpoint = int * rec_declaration
 
 (***************************)
 (* hash-consing functions  *)                         
@@ -158,7 +177,6 @@ let comp_term t1 t2 =
   | IsMeta m1, IsMeta m2 -> m1 = m2
   | IsVar id1, IsVar id2 -> id1 == id2
   | IsSort s1, IsSort s2 -> s1 == s2
-  | IsXtra s1, IsXtra s2 -> s1 == s2
   | IsCast (c1,t1), IsCast (c2,t2) -> c1 == c2 & t1 == t2
   | IsProd (n1,t1,c1), IsProd (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
   | IsLambda (n1,t1,c1), IsLambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
@@ -185,7 +203,6 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t =
   | IsRel _ | IsMeta _ -> t
   | IsVar x -> IsVar (sh_id x)
   | IsSort s -> IsSort (sh_sort s)
-  | IsXtra s -> IsXtra (sh_str s)
   | IsCast (c,t) -> IsCast (sh_rec c, sh_rec t)
   | IsProd (na,t,c) -> IsProd (sh_na na, sh_rec t, sh_rec c)
   | IsLambda (na,t,c) -> IsLambda (sh_na na, sh_rec t, sh_rec c)
@@ -228,9 +245,6 @@ let mkMeta  n =  IsMeta n
 (* Constructs a Variable named id *)
 let mkVar id = IsVar id
 
-(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
-let mkXtra s = IsXtra s
-
 (* Construct a type *)
 let mkSort s = IsSort s
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
@@ -283,6 +297,7 @@ let mkFix fix = IsFix fix
 let mkCoFix cofix = IsCoFix cofix
 
 let kind_of_term c = c
+let mk_constr c = c
 
 (*
 end
@@ -346,11 +361,6 @@ let destVar c = match kind_of_term c with
   | IsVar id -> id
   | _ -> invalid_arg "destVar"
 
-(* Destructs an XTRA *)
-let destXtra c = match kind_of_term c with
-  | IsXtra s -> s
-  | _ -> invalid_arg "destXtra"
-
 (* Destructs a type *)
 let isSort c = match kind_of_term c with
   | IsSort s -> true
@@ -502,7 +512,7 @@ let destCoFix c = match kind_of_term c with
    the usual representation of the constructions; it is not recursive *)
 
 let fold_constr f acc c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> acc
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> acc
   | IsCast (c,t) -> f (f acc c) t
   | IsProd (_,t,c) -> f (f acc t) c
   | IsLambda (_,t,c) -> f (f acc t) c
@@ -526,7 +536,7 @@ let fold_constr f acc c = match kind_of_term c with
    each binder traversal; it is not recursive *)
 
 let fold_constr_with_binders g f n acc c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> acc
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> acc
   | IsCast (c,t) -> f n (f n acc c) t
   | IsProd (_,t,c) -> f (g n) (f n acc t) c
   | IsLambda (_,t,c) -> f (g n) (f n acc t) c
@@ -549,7 +559,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
    not specified *)
 
 let iter_constr f c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> ()
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> ()
   | IsCast (c,t) -> f c; f t
   | IsProd (_,t,c) -> f t; f c
   | IsLambda (_,t,c) -> f t; f c
@@ -570,7 +580,7 @@ let iter_constr f c = match kind_of_term c with
    subterms are processed is not specified *)
 
 let iter_constr_with_binders g f n c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> ()
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> ()
   | IsCast (c,t) -> f n c; f n t
   | IsProd (_,t,c) -> f n t; f (g n) c
   | IsLambda (_,t,c) -> f n t; f (g n) c
@@ -591,7 +601,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with
    not specified *)
 
 let map_constr f c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
   | IsCast (c,t) -> mkCast (f c, f t)
   | IsProd (na,t,c) -> mkProd (na, f t, f c)
   | IsLambda (na,t,c) -> mkLambda (na, f t, f c)
@@ -612,7 +622,7 @@ let map_constr f c = match kind_of_term c with
    subterms are processed is not specified *)
 
 let map_constr_with_binders g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
   | IsCast (c,t) -> mkCast (f l c, f l t)
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
@@ -637,7 +647,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with
    and the order with which subterms are processed is not specified *)
 
 let map_constr_with_named_binders g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
   | IsCast (c,t) -> mkCast (f l c, f l t)
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
@@ -688,7 +698,7 @@ let array_map_left_pair f a g b =
   end
 
 let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
   | IsCast (c,t) -> let c' = f l c in mkCast (c', f l t)
   | IsProd (na,t,c) -> let t' = f l t in mkProd (na, t', f (g l) c)
   | IsLambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c)
@@ -714,7 +724,7 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
 
 (* strong *)
 let map_constr_with_full_binders g f l c = match kind_of_term c with
-  | IsRel _ | IsMeta _ | IsVar _   | IsSort _  | IsXtra _ -> c
+  | IsRel _ | IsMeta _ | IsVar _   | IsSort _ -> c
   | IsCast (c,t) -> mkCast (f l c, f l t)
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c)
@@ -744,7 +754,6 @@ let compare_constr f c1 c2 =
   | IsMeta m1, IsMeta m2 -> m1 = m2
   | IsVar id1, IsVar id2 -> id1 = id2
   | IsSort s1, IsSort s2 -> s1 = s2
-  | IsXtra s1, IsXtra s2 -> s1 = s2
   | IsCast (c1,_), _ -> f c1 c2
   | _, IsCast (c2,_) -> f c1 c2
   | IsProd (_,t1,c1), IsProd (_,t2,c2) -> f t1 t2 & f c1 c2
@@ -858,35 +867,6 @@ let noccur_with_meta n m term =
 (*      Lifting      *)
 (*********************)
 
-(* Explicit lifts and basic operations *)
-type lift_spec =
-  | ELID
-  | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
-  | ELLFT of int * lift_spec  (* ELLFT(n,l)  == apply l to de Bruijn > n *)
-                            (*                 i.e under n binders *)
-
-(* compose a relocation of magnitude n *)
-let rec el_shft n = function
-  | ELSHFT(el,k) -> el_shft (k+n) el
-  | el -> if n = 0 then el else ELSHFT(el,n)
-
-
-(* cross n binders *)
-let rec el_liftn n = function
-  | ELID -> ELID
-  | ELLFT(k,el) -> el_liftn (n+k) el
-  | el -> if n=0 then el else ELLFT(n, el)
-
-let el_lift el = el_liftn 1 el
-
-(* relocation of de Bruijn n in an explicit lift *)
-let rec reloc_rel n = function
-  | ELID -> n
-  | ELLFT(k,el) ->
-      if n <= k then n else (reloc_rel (n-k) el) + k
-  | ELSHFT(el,k) -> (reloc_rel (n+k) el)
-
-
 (* The generic lifting function *)
 let rec exliftn el c = match kind_of_term c with
   | IsRel i -> mkRel(reloc_rel i el)
@@ -1007,9 +987,6 @@ let mkMeta = mkMeta
 (* Constructs a Variable named id *)
 let mkVar = mkVar
 
-(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
-let mkXtra = mkXtra
-
 (* Construct a type *)
 let mkSort   = mkSort
 let mkProp   = mkSort mk_Prop
@@ -1239,6 +1216,15 @@ let prod_appvect t nL = Array.fold_left prod_app t nL
 let prod_applist t nL = List.fold_left prod_app t nL
 
 
+(* [Rel (n+m);...;Rel(n+1)] *)
+let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
+
+let rel_list n m = 
+  let rec reln l p = 
+    if p>m then l else reln (mkRel(n+p)::l) (p+1)
+  in 
+  reln [] 1
+
 (*********************************)
 (* Other term destructors        *)
 (*********************************)
@@ -1693,7 +1679,6 @@ type constr_operator =
   | OpMutConstruct of constructor_path
   | OpMutCase of case_info
   | OpRec of fix_kind * name list
-  | OpXtra of string
 
 let splay_constr c = match kind_of_term c with
   | IsRel n                    -> OpRel n, [||]
@@ -1704,7 +1689,7 @@ let splay_constr c = match kind_of_term c with
   | IsProd (x, t1, t2)         -> OpProd x, [|t1;t2|]
   | IsLambda (x, t1, t2)       -> OpLambda x, [|t1;t2|]
   | IsLetIn (x, b, t1, t2)     -> OpLetIn x, [|b;t1;t2|]
-  | IsApp (f,a)               -> OpApp, Array.append [|f|] a
+  | IsApp (f,a)                -> OpApp, Array.append [|f|] a
   | IsConst (sp, a)            -> OpConst sp, a
   | IsEvar (sp, a)             -> OpEvar sp, a
   | IsMutInd (ind_sp, l)       -> OpMutInd ind_sp, l
@@ -1712,7 +1697,6 @@ let splay_constr c = match kind_of_term c with
   | IsMutCase (ci,p,c,bl)      -> OpMutCase ci, Array.append [|p;c|] bl
   | IsFix (fi,(tl,lna,bl))     -> OpRec (RFix fi,lna), Array.append tl bl
   | IsCoFix (fi,(tl,lna,bl))   -> OpRec (RCoFix fi,lna), Array.append tl bl
-  | IsXtra s                   -> OpXtra s, [||]
 
 let gather_constr = function
   | OpRel n, [||]  -> mkRel n
@@ -1737,7 +1721,6 @@ let gather_constr = function
   | OpRec (RCoFix i,lna), a ->
       let n = Array.length a / 2 in
       mkCoFix (i,(Array.sub a 0 n, lna, Array.sub a n n))
-  | OpXtra s, [||] -> mkXtra s
   | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">]
 
 let rec mycombine l1 l3 =
@@ -1778,7 +1761,6 @@ let splay_constr_with_binders c = match kind_of_term c with
 		   (List.rev lna)
 		   (Array.to_list (Array.mapi lift tl)) in
       OpRec (RCoFix fi,lna), ctxt, bl
-  | IsXtra s -> OpXtra s, [], [||]
 
 let gather_constr_with_binders = function
   | OpRel n, [], [||]  -> mkRel n
@@ -1805,7 +1787,6 @@ let gather_constr_with_binders = function
       let (lna, tl) = mysplit ctxt in
       let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in
       mkCoFix (i,(tl, List.rev lna, bl))
-  | OpXtra s, [], [||] -> mkXtra s
   | _  -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">]
 
 let generic_fold_left f acc bl tl =
diff --git a/kernel/term.mli b/kernel/term.mli
index 858ba2465..8672f10a4 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -31,6 +31,26 @@ type case_printing =
 (* the integer is the number of real args, needed for reduction *)
 type case_info = int array * case_printing
 
+(* Concrete type for making pattern-matching. *)
+module Polymorph :
+sig
+(* [constr array] is an instance matching definitional [named_context] in
+   the same order (i.e. last argument first) *)
+type 'constr existential = existential_key * 'constr array
+type 'constr constant = constant_path * 'constr array
+type 'constr constructor = constructor_path * 'constr array
+type 'constr inductive = inductive_path * 'constr array
+type ('constr, 'types) rec_declaration =
+    'types array * name list * 'constr array
+type ('constr, 'types) fixpoint =
+    (int array * int) * ('constr, 'types) rec_declaration
+type ('constr, 'types) cofixpoint =
+    int * ('constr, 'types) rec_declaration
+
+(* [IsVar] is used for named variables and [IsRel] for variables as
+   de Bruijn indices. *)
+end 
+
 (********************************************************************)
 (* type of global reference *)
 
@@ -74,46 +94,39 @@ type arity = rel_declaration list * sorts
   manipulation of terms. Some of these functions may be overlapped with
   previous ones. *)
 
-(* Concrete type for making pattern-matching. *)
+open Polymorph
+type ('constr, 'types) kind_of_term =
+  | IsRel          of int
+  | IsMeta         of int
+  | IsVar          of identifier
+  | IsSort         of sorts
+  | IsCast         of 'constr * 'constr
+  | IsProd         of name * 'types * 'constr 
+  | IsLambda       of name * 'types * 'constr
+  | IsLetIn        of name * 'constr * 'types * 'constr
+  | IsApp          of 'constr * 'constr array
+  | IsEvar         of 'constr existential
+  | IsConst        of 'constr constant
+  | IsMutInd       of 'constr inductive
+  | IsMutConstruct of 'constr constructor
+  | IsMutCase      of case_info * 'constr * 'constr * 'constr array
+  | IsFix          of ('constr, 'types) fixpoint
+  | IsCoFix        of ('constr, 'types) cofixpoint
 
-(* [constr array] is an instance matching definitional [named_context] in
-   the same order (i.e. last argument first) *)
 type existential = existential_key * constr array
 type constant = constant_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
-type rec_declaration = constr array * name list * constr array
+type rec_declaration = types array * name list * constr array
 type fixpoint = (int array * int) * rec_declaration
 type cofixpoint = int * rec_declaration
 
-(* [IsVar] is used for named variables and [IsRel] for variables as
-   de Bruijn indices. *)
-
-type kind_of_term =
-  | IsRel          of int
-  | IsMeta         of int
-  | IsVar          of identifier
-  | IsXtra         of string
-  | IsSort         of sorts
-  | IsCast         of constr * constr
-  | IsProd         of name * types * constr 
-  | IsLambda       of name * types * constr
-  | IsLetIn        of name * constr * types * constr
-  | IsApp         of constr * constr array
-  | IsEvar         of existential
-  | IsConst        of constant
-  | IsMutInd       of inductive
-  | IsMutConstruct of constructor
-  | IsMutCase      of case_info * constr * constr * constr array
-  | IsFix          of fixpoint
-  | IsCoFix        of cofixpoint
-
 (* User view of [constr]. For [IsApp], it is ensured there is at
    least one argument and the function is not itself an applicative
    term *)
 
-val kind_of_term : constr -> kind_of_term
-
+val kind_of_term : constr -> (constr, types) kind_of_term
+val mk_constr : (constr, types) kind_of_term -> constr
 
 (*s Term constructors. *)
 
@@ -126,9 +139,6 @@ val mkMeta : int -> constr
 (* Constructs a Variable *)
 val mkVar : identifier -> constr
 
-(* Construct an  [XTRA] term. *)
-val mkXtra : string -> constr
-
 (* Construct a type *)
 val mkSort : sorts -> constr
 val mkProp : constr
@@ -252,9 +262,6 @@ val isMeta : constr -> bool
 (* Destructs a variable *)
 val destVar : constr -> identifier
 
-(* Destructs an XTRA *)
-val destXtra : constr -> string
-
 (* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether 
    [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *)
 val destSort : constr -> sorts
@@ -478,17 +485,9 @@ val subst_vars : identifier list -> constr -> constr
    if two names are identical, the one of least indice is keeped *)
 val substn_vars : int -> identifier list -> constr -> constr
 
-(*s Compact representation of implicit lifts. \\
-   [ELSHFT(l,n)] == lift of [n], then apply [lift l].
-  [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
-type lift_spec =
-  | ELID
-  | ELSHFT of lift_spec * int
-  | ELLFT of int * lift_spec
-val el_shft : int -> lift_spec -> lift_spec
-val el_liftn : int -> lift_spec -> lift_spec
-val el_lift : lift_spec -> lift_spec
-val reloc_rel : int -> lift_spec -> int
+(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
+val rel_vect : int -> int -> constr array
+val rel_list : int -> int -> constr list
 
 (*s Occur check functions. *)                         
 
@@ -552,19 +551,22 @@ type constr_operator =
   | OpMutConstruct of constructor_path
   | OpMutCase of case_info
   | OpRec of fix_kind * Names.name list
-  | OpXtra of string
+
 
 val splay_constr : constr -> constr_operator * constr array
 val gather_constr : constr_operator * constr array -> constr
-
+(*
+val splay_constr : ('a,'a)kind_of_term -> constr_operator * 'a array
+val gather_constr : constr_operator * 'a array -> ('a,'a) kind_of_term
+*)
 val splay_constr_with_binders : constr ->
-      constr_operator * (name * constr option * constr) list * constr array
+      constr_operator * rel_declaration list * constr array
 val gather_constr_with_binders : 
-  constr_operator * (name * constr option * constr) list * constr array
+  constr_operator * rel_declaration list * constr array
   -> constr
 
 val generic_fold_left :
-  ('a -> constr -> 'a) -> 'a -> (name * constr option * constr) list
+  ('a -> constr -> 'a) -> 'a -> rel_declaration list
       -> constr array -> 'a
 
 (*s Functionals working on the immediate subterm of a construction *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 65be6547b..7b6e58c83 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -679,8 +679,6 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	| IsMeta _ -> true
 
 	| IsVar _ | IsSort _ ->  List.for_all (check_rec_call env n lst) l
-
-	| IsXtra _ ->  List.for_all (check_rec_call env n lst) l
      )
 
      and check_rec_call_fix_body env n lst decr recArgsDecrArg body =
@@ -885,7 +883,7 @@ let type_fixpoint env sigma lna lar vdefj =
 let control_only_guard env sigma = 
   let rec control_rec c = match kind_of_term c with
     | IsRel _ | IsVar _    -> ()
-    | IsSort _ | IsMeta _ | IsXtra _ -> ()
+    | IsSort _ | IsMeta _ -> ()
     | IsCoFix (_,(tys,_,bds) as cofix) ->
 	check_cofix env sigma cofix;
 	Array.iter control_rec tys;
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
new file mode 100644
index 000000000..15a50bcc4
--- /dev/null
+++ b/pretyping/cbv.ml
@@ -0,0 +1,396 @@
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Term
+open Names
+open Environ
+open Instantiate
+open Univ
+open Evd
+open Closure
+open Esubst
+
+(**** 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 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
+ *          only when the abstraction is applied, and then we use the rule
+ *                  ([S]([x:a]b) c) --> [S.c]b
+ *          This corresponds to the usual strategy of weak reduction
+ *  FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under
+ *          the substitution S, and then applied to args. Here again,
+ *          weak reduction.
+ *  CONSTR(n,(sp,i),vars,args) is the n-th constructor of the i-th
+ *          inductive type sp.
+ *
+ * Note that any term has not an equivalent in cbv_value: for example,
+ * a product (x:A)B must be in normal form because only VAL may
+ * represent it, and the argument of VAL is always in normal
+ * form. This remark precludes coding a head reduction with these
+ * functions. Anyway, does it make sense to head reduce with a
+ * call-by-value strategy ?
+ *)
+type cbv_value =
+  | VAL of int * constr
+  | LAM of name * constr * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value list
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
+  | CONSTR of int * inductive_path * cbv_value array * cbv_value list
+
+(* les vars pourraient etre des constr,
+   cela permet de retarder les lift: utile ?? *) 
+
+(* relocation of a value; used when a value stored in a context is expanded
+ * in a larger context. e.g.  [%k (S.t)](k+1) --> [^k]t  (t is shifted of k)
+ *)
+let rec shift_value n = function
+  | VAL (k,v) -> VAL ((k+n),v)
+  | LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s))
+  | FIXP (fix,s,args) ->
+      FIXP (fix,subs_shft (n,s), List.map (shift_value n) args)
+  | COFIXP (cofix,s,args) ->
+      COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args)
+  | CONSTR (i,spi,vars,args) ->
+      CONSTR (i, spi, Array.map (shift_value n) vars,
+              List.map (shift_value n) args)
+	
+
+(* Contracts a fixpoint: given a fixpoint and a substitution,
+ * returns the corresponding fixpoint body, and the substitution in which
+ * it should be evaluated: its first variables are the fixpoint bodies
+ * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
+ *    -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
+ *)
+let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
+  let make_body j = FIXP(((reci,j),bodies), env, []) in
+  let n = Array.length bds in
+  let rec subst_bodies_from_i i subs =
+    if i=n then subs
+    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
+  in       
+  subst_bodies_from_i 0 env, bds.(i)
+
+let contract_cofixp env (i,(_,_,bds as bodies)) =
+  let make_body j = COFIXP((j,bodies), env, []) in
+  let n = Array.length bds in
+  let rec subst_bodies_from_i i subs =
+    if i=n then subs
+    else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs))
+  in       
+  subst_bodies_from_i 0 env, bds.(i)
+
+
+(* type of terms with a hole. This hole can appear only under App or Case.
+ *   TOP means the term is considered without context
+ *   APP(l,stk) means the term is applied to l, and then we have the context st
+ *      this corresponds to the application stack of the KAM.
+ *      The members of l are values: we evaluate arguments before the function.
+ *   CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk
+ *      t is the type of the case and br are the branches, all of them under
+ *      the subs S, pat is information on the patterns of the Case
+ *      (Weak reduction: we propagate the sub only when the selected branch
+ *      is determined)
+ *
+ * Important remark: the APPs should be collapsed:
+ *    (APP (l,(APP ...))) forbidden
+ *)
+
+type cbv_stack =
+  | TOP
+  | APP of cbv_value list * cbv_stack
+  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+
+(* Adds an application list. Collapse APPs! *)
+let stack_app appl stack =
+  match (appl, stack) with
+    | ([], _)            -> stack
+    | (_, APP(args,stk)) -> APP(appl@args,stk)
+    | _                  -> APP(appl, stack)
+
+(* Tests if we are in a case (modulo some applications) *)
+let under_case_stack = function
+  | (CASE _ | APP(_,CASE _)) -> true
+  | _ -> false
+
+(* Tells if the reduction rk is allowed by flags under a given stack.
+ * The stack is useful when flags is (SIMPL,r) because in that case,
+ * we perform bdi-reduction under the Case, or r-reduction otherwise
+ *)
+let red_allowed flags stack rk =
+  if under_case_stack stack then 
+    red_under flags rk
+  else 
+    red_top flags rk
+
+let red_allowed_ref flags stack = function
+  | FarRelBinding _ -> red_allowed flags stack DELTA
+  | VarBinding id -> red_allowed flags stack (VAR id)
+  | 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
+ *)
+let strip_appl head stack =
+  match head with
+    | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack)
+    | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack)
+    | CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack)
+    | _ -> (head, stack)
+
+
+(* 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.
+ *)
+let reduce_const_body redfun v stk =
+  if under_case_stack stk then strip_appl (redfun v) stk else strip_appl v stk
+ 
+
+(* Tests if fixpoint reduction is possible. A reduction function is given as
+   argument *)
+let rec check_app_constr redfun = function
+  | ([], _) -> false
+  | ((CONSTR _)::_, 0) -> true
+  | (t::_, 0) -> (* TODO: partager ce calcul *)
+      (match redfun t with
+         | CONSTR _ -> true
+         | _ -> false)
+  | (_::l, n) -> check_app_constr redfun (l,(pred n))
+	
+let fixp_reducible redfun flgs ((reci,i),_) stk =
+  if red_allowed flgs stk IOTA then
+    match stk with               (* !!! for Acc_rec: reci.(i) = -2 *)
+      | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i))
+      | _ -> false
+  else 
+    false
+
+let cofixp_reducible redfun flgs _ stk =
+  if red_allowed flgs stk IOTA then
+    match stk with
+      | (CASE _ | APP(_,CASE _)) -> true
+      | _ -> false
+  else 
+    false
+
+let mindsp_nparams env (sp,i) =
+  let mib = lookup_mind sp env in
+  (Declarations.mind_nth_type_packet mib i).Declarations.mind_nparams
+
+(* The main recursive functions
+ *
+ * Go under applications and cases (pushed in the stack), expand head
+ * constants or substitued de Bruijn, and try to make appear a
+ * constructor, a lambda or a fixp in the head. If not, it is a value
+ * and is completely computed here. The head redexes are NOT reduced:
+ * the function returns the pair of a cbv_value and its stack.  *
+ * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
+ * argument is [].  Because we must put all the applied terms in the
+ * stack. *)
+
+let rec norm_head info env t stack =
+  (* no reduction under binders *)
+  match kind_of_term t with
+  (* stack grows (remove casts) *)
+  | IsApp (head,args) -> (* Applied terms are normalized immediately;
+                        they could be computed when getting out of the stack *)
+      let nargs = Array.map (cbv_stack_term info TOP env) args in
+      norm_head info env head (stack_app (Array.to_list nargs) stack)
+  | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
+  | IsCast (ct,_) -> norm_head info env ct stack
+
+  (* constants, axioms
+   * the first pattern is CRUCIAL, n=0 happens very often:
+   * 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 env) v stack
+                | Inl (n,v) ->
+                    reduce_const_body
+                      (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-p) info env stack (FarRelBinding p))
+
+  | IsVar id -> norm_head_ref 0 info env stack (VarBinding id)
+
+  | IsConst (sp,vars) ->
+      let normt = (sp,Array.map (cbv_norm_term info env) vars) in
+      norm_head_ref 0 info env stack (ConstBinding normt)
+
+  | IsEvar ev -> norm_head_ref 0 info env stack (EvarBinding (ev,env))
+
+  | IsLetIn (x, b, t, c) ->
+      (* zeta means letin are contracted; delta without zeta means we *)
+      (* allow substitution but leave let's in place *)
+      let zeta = red_allowed (info_flags info) stack ZETA in
+      let env' =
+	if zeta or red_allowed (info_flags info) stack DELTA then 
+	  subs_cons (cbv_stack_term info TOP env b,env)
+	else
+	  subs_lift env in
+      if zeta then
+        norm_head info env' c stack
+      else
+	let normt =
+	  mkLetIn (x, cbv_norm_term info env b,
+		   cbv_norm_term info env t,
+		   cbv_norm_term info env' c) in
+	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
+
+  (* non-neutral cases *)
+  | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack)
+  | IsFix fix -> (FIXP(fix,env,[]), stack)
+  | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack)
+  | IsMutConstruct ((spi,i),vars) ->
+      (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack)
+
+  (* neutral cases *)
+  | (IsSort _ | IsMeta _) -> (VAL(0, t), stack)
+  | IsMutInd (sp,vars) -> 
+      (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack)
+  | IsProd (x,t,c) -> 
+      (VAL(0, mkProd (x, cbv_norm_term info env t,
+		      cbv_norm_term info (subs_lift env) c)),
+	     stack)
+
+and norm_head_ref k info env stack normt =
+  if red_allowed_ref (info_flags info) 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 info normt), stack)
+  else (VAL(0,make_constr_ref k info normt), stack)
+
+and make_constr_ref n info = function
+  | FarRelBinding p -> mkRel (n+p)
+  | VarBinding id -> mkVar id
+  | EvarBinding ((ev,args),env) ->
+      mkEvar (ev,Array.map (cbv_norm_term info env) args)
+  | ConstBinding cst -> mkConst cst
+
+(* 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.
+ * If so, recursive call to reach the real head normal form.  If not,
+ * we build a value. 
+ *)
+and cbv_stack_term info stack env t =
+  match norm_head info env t stack with
+    (* a lambda meets an application -> BETA *)
+    | (LAM (x,a,b,env), APP (arg::args, stk))
+      when red_allowed (info_flags info) stk BETA ->
+        let subs = subs_cons (arg,env) in
+          cbv_stack_term info (stack_app args stk) subs b
+
+    (* a Fix applied enough -> IOTA *)
+    | (FIXP(fix,env,_), stk)
+        when fixp_reducible (cbv_norm_more info env) (info_flags info) 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 env) (info_flags info) cofix stk->
+        let (envf,redfix) = contract_cofixp env cofix in
+        cbv_stack_term info stk envf redfix
+
+    (* constructor in a Case -> IOTA
+       (use red_under because we know there is a Case) *)
+    | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,(arity,_),env,stk)))
+            when red_under (info_flags info) IOTA ->
+	let ncargs = arity.(n-1) in
+	let real_args = list_lastn ncargs args in
+        cbv_stack_term info (stack_app real_args stk) env br.(n-1)
+         
+    (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
+    | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk))
+                  when red_under (info_flags info) IOTA ->
+                    cbv_stack_term info stk env br.(n-1)
+
+    (* may be reduced later by application *)  
+    | (head, TOP) -> head
+    | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl) 
+    | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) 
+    | (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl)
+
+    (* definitely a value *)
+    | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
+
+
+(* if we are in SIMPL mode, maybe v isn't reduced enough *)
+and cbv_norm_more info env v =
+  match (v, (info_flags info)) with
+    | (VAL(k,t), ((SIMPL|WITHBACK),_)) ->
+        cbv_stack_term (infos_under info) TOP (subs_shft (k,env)) t
+    | _ -> v
+
+
+(* When we are sure t will never produce a redex with its stack, we
+ * normalize (even under binders) the applied terms and we build the
+ * final term
+ *)
+and apply_stack info t = function
+  | TOP -> t
+  | APP (args,st) ->
+      apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st
+  | CASE (ty,br,ci,env,st) ->
+      apply_stack info
+        (mkMutCase (ci, cbv_norm_term info env ty, t,
+		    Array.map (cbv_norm_term info env) br))
+        st
+
+
+(* performs the reduction on a constr, and returns a constr *)
+and cbv_norm_term info env t =
+  (* reduction under binders *)
+  cbv_norm_value info (cbv_stack_term info TOP env t)
+
+(* reduction of a cbv_value to a constr *)
+and cbv_norm_value info = function (* reduction under binders *)
+  | VAL (n,v) -> lift n v
+  | LAM (x,a,b,env) ->
+      mkLambda (x, cbv_norm_term info env a,
+		cbv_norm_term info (subs_lift env) b)
+  | FIXP ((lij,(lty,lna,bds)),env,args) ->
+      applistc
+        (mkFix (lij,
+		(Array.map (cbv_norm_term info env) lty, lna, 
+		 Array.map (cbv_norm_term info 
+			      (subs_liftn (Array.length lty) env)) bds)))
+        (List.map (cbv_norm_value info) args)
+  | COFIXP ((j,(lty,lna,bds)),env,args) ->
+      applistc
+        (mkCoFix (j,
+		  (Array.map (cbv_norm_term info env) lty, lna, 
+		   Array.map (cbv_norm_term info 
+				(subs_liftn (Array.length lty) env)) bds)))
+        (List.map (cbv_norm_value info) args)
+  | CONSTR (n,spi,vars,args) ->
+      applistc
+        (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars))
+        (List.map (cbv_norm_value info) args)
+
+(* with profiling *)
+let cbv_norm infos constr =
+  with_stats (lazy (cbv_norm_term infos (ESID 0) constr))
+
+
+type 'a cbv_infos = (cbv_value, 'a) infos
+
+(* constant bodies are normalized at the first expansion *)
+let create_cbv_infos flgs env sigma =
+  create
+    (fun old_info s c -> cbv_stack_term old_info TOP s c)
+    flgs
+    env
+    sigma
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
new file mode 100644
index 000000000..08e067f5a
--- /dev/null
+++ b/pretyping/cbv.mli
@@ -0,0 +1,55 @@
+
+(*i $Id$ i*)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Evd
+open Environ
+open Closure
+open Esubst
+(*i*)
+
+(***********************************************************************)
+(*s Call-by-value reduction *)
+
+(* Entry point for cbv normalization of a constr *)
+type 'a cbv_infos
+val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos
+val cbv_norm : 'a cbv_infos -> constr -> constr
+
+(***********************************************************************)
+(*i This is for cbv debug *)
+type cbv_value =
+  | VAL of int * constr
+  | LAM of name * constr * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value list
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value list
+  | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
+
+val shift_value : int -> cbv_value -> cbv_value
+
+type cbv_stack =
+  | TOP
+  | APP of cbv_value list * cbv_stack
+  | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
+
+val stack_app : cbv_value list -> cbv_stack -> cbv_stack
+val under_case_stack : cbv_stack -> bool
+val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
+
+val red_allowed : flags -> cbv_stack -> red_kind -> bool
+val reduce_const_body :
+  (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack
+
+(* recursive functions... *)
+val cbv_stack_term : 'a cbv_infos ->
+  cbv_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 subs -> cbv_value -> cbv_value
+val norm_head : 'a cbv_infos ->
+  cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack
+val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr
+val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
+(* End of cbv debug section i*)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dc4330b5e..e376abb25 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -283,9 +283,6 @@ let rec detype avoid env t =
 	 in RVar (dummy_loc, id_of_string s))
     | IsMeta n -> RMeta (dummy_loc, n)
     | IsVar id -> RVar (dummy_loc, id)
-    | IsXtra s -> warning "bdize: Xtra should no longer occur in constr";
-	RVar(dummy_loc, id_of_string ("XTRA"^s))
-        (* ope("XTRA",((str s):: pl@(List.map detype cl)))*) 
     | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
     | IsSort (Type _) -> RSort (dummy_loc,RType)
     | IsCast (c1,c2) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8dab70441..82746d287 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -257,8 +257,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 		 bds1 bds2)
 	    & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-	| (IsMeta _ | IsXtra _ | IsLambda _), _ -> false
-	| _, (IsMeta _ | IsXtra _ | IsLambda _) -> false
+	| (IsMeta _ | IsLambda _), _ -> false
+	| _, (IsMeta _ | IsLambda _) -> false
 
 	| (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false
 	| _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 625e28d56..b83019b45 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -269,7 +269,7 @@ let rec sub_match nocc pat c =
       let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
       (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)))
   | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _
-  | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ ->
+  | IsRel _|IsMeta _|IsVar _|IsSort _ ->
     (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with
     | PatternMatchingFailure -> raise (NextOccurrence nocc)
     | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
@@ -320,7 +320,6 @@ let rec pattern_of_constr t =
     | IsFix f -> PFix f
     | IsCoFix _ ->
 	error "pattern_of_constr: (co)fix currently not supported"
-    | IsXtra _   -> anomaly "No longer supported"
 
 and pattern_of_ref ref inst =
   let args = Declare.extract_instance ref inst in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index ee8c1f764..657f3d1e0 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -73,7 +73,6 @@ let rec type_of env cstr=
 			  (Array.to_list args))
     | IsCast (c,t) -> t
     | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr)
-    | IsXtra _ -> error "type_of: Unexpected constr"
 
 and sort_of env t = 
   match kind_of_term t with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index baf120029..1b4b89f8b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -10,6 +10,7 @@ open Environ
 open Reduction
 open Closure
 open Instantiate
+open Cbv
 
 (************************************************************************)
 (* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick   *)
@@ -584,7 +585,7 @@ let rec substlin env name n ol c =
     | IsCoFix _ -> 
         (warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
 
-    | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _
+    | (IsRel _|IsMeta _|IsVar _|IsSort _
       |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c)
 	
 let unfold env sigma name =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d3f7eb0ed..afdaf5823 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -115,8 +115,6 @@ let rec execute mf env sigma cstr =
         let j, _ = cast_rel env sigma cj tj in
 	j
 	  
-    | IsXtra _ -> anomaly "Typing: found an Extra"
-	  
 and execute_fix mf env sigma lar lfi vdef =
   let larj = execute_array mf env sigma lar in
   let lara = Array.map (assumption_of_judgment env sigma) larj in
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 8ec991c0f..6c87782fc 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -213,8 +213,7 @@ let rec compute_metamap env c = match kind_of_term c with
       	TH (c,[],[])
 
   (* Autres cas. *)
-  | IsXtra _|IsCoFix _ ->
-      invalid_arg "Tcc.compute_metamap"
+  | IsCoFix _ -> invalid_arg "Tcc.compute_metamap"
 
 
 (*  tcc_aux : term_with_holes -> tactic