subst. explicites avec vecteurs

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

7 files changed, 137 insertions, 125 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index c5a5b9ffa..ff456b93c 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -645,9 +645,9 @@ and compact_v acc s v k i =
 let optimise_closure env c =
   if is_subs_id env then (env,c) else
     let (c',(_,s)) = compact_constr (0,[]) c 1 in
-    let env' = List.fold_left
-      (fun subs i -> subs_cons (clos_rel env i, subs)) (ESID 0) s in
-    (env',c')
+    let env' =
+      Array.map (fun i -> clos_rel env i) (Array.of_list s) in
+    (subs_cons (env', ESID 0),c')
 
 let mk_lambda env t =
   let (env,t) = optimise_closure env t in
@@ -876,18 +876,14 @@ let rec get_args n tys f e stk =
         get_args n tys f (subs_shft (k,e)) s
     | Zapp l :: s ->
         let na = Array.length l in
-        if n == na then
-          let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e l in
-          (Inl e',s)
+        if n == na then (Inl (subs_cons(l,e)),s)
         else if n < na then (* more arguments *)
           let args = Array.sub l 0 n in
           let eargs = Array.sub l n (na-n) in
-          let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e args in
-          (Inl e', Zapp eargs :: s)
+          (Inl (subs_cons(args,e)), Zapp eargs :: s)
         else (* more lambdas *)
           let (_,etys) = list_chop na tys in
-          let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e l in
-          get_args (n-na) etys f e' s
+          get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
 
@@ -939,13 +935,7 @@ let contract_fix_vect fix =
 	   env, Array.length bds)
       | _ -> assert false
   in
-  let rec subst_bodies_from_i i env =
-    if i = nfix then
-      (env, thisbody)
-    else
-      subst_bodies_from_i (i+1) (subs_cons (make_body i, env))
-  in       
-  subst_bodies_from_i 0 env
+  (subs_cons(Array.init nfix make_body, env), thisbody)
 
 
 (*********************************************************************)
@@ -1025,7 +1015,7 @@ let rec knr info m stk =
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
   | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
-      knit info (subs_cons(v,e)) bd stk
+      knit info (subs_cons([|v|],e)) bd stk
   | _ -> (m,stk)
 
 (* Computes the weak head normal form of a term *)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 7662a2f8b..dc29e4e98 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -55,7 +55,10 @@ let rec is_lift_id = function
 (* (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 *)
+  | CONS of 'a array * 'a subs
+                           (* CONS([|t1..tn|],S)  =
+                              (S.t1...tn)    parallel substitution
+                              beware of the order *)
   | 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) *)
@@ -64,7 +67,7 @@ type 'a subs =
  * Needn't be recursive if we always use these functions
  *)
 
-let subs_cons(x,s) = CONS(x,s)
+let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s)
 
 let subs_liftn n = function
   | ESID p        -> ESID (p+n) (* bounded identity lifted extends by p *)
@@ -85,11 +88,12 @@ let subs_shift_cons = function
 | (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 *)
+(* Tests whether a substitution is 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
+  | CONS(x,s)  -> Array.length x = 0 && is_subs_id s
   | _          -> false
 
 (* Expands de Bruijn k in the explicit substitution subs
@@ -108,14 +112,15 @@ let rec is_subs_id = function
  * 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))
+  match subs with
+    | CONS (def,_) when k <= Array.length def
+                           -> Inl(lams,def.(Array.length def - k))
+    | CONS (v,l)           -> exp_rel lams (k - Array.length v) 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
 
@@ -124,9 +129,20 @@ let rec comp mk_cl s1 s2 =
     | _, ESID _ -> s1
     | ESID _, _ -> s2
     | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
-    | _, CONS(x,s') -> CONS(mk_cl(s1,x), comp mk_cl s1 s')
-    | CONS(x,s), SHIFT(k,s') -> comp mk_cl s (subs_shft(k-1, s'))
-    | CONS(x,s), LIFT(k,s') -> CONS(x,comp mk_cl s (subs_liftn (k-1) s'))
+    | _, CONS(x,s') ->
+        CONS(Array.map (fun t -> mk_cl(s1,t)) x, comp mk_cl s1 s')
+    | CONS(x,s), SHIFT(k,s') ->
+        let lg = Array.length x in
+        if k == lg then comp mk_cl s s'
+        else if k > lg then comp mk_cl s (SHIFT(k-lg, s'))
+        else comp mk_cl (CONS(Array.sub x 0 (lg-k), s)) s'
+    | CONS(x,s), LIFT(k,s') ->
+        let lg = Array.length x in
+        if k == lg then CONS(x, comp mk_cl s s')
+        else if k > lg then CONS(x, comp mk_cl s (LIFT(k-lg, s')))
+        else
+          CONS(Array.sub x (lg-k) k,
+               comp mk_cl (CONS(Array.sub x 0 (lg-k),s)) s')
     | LIFT(k,s), SHIFT(k',s') ->
         if k<k'
         then subs_shft(k, comp mk_cl s (subs_shft(k'-k, s')))
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index cd9c16907..68f5f2201 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -22,21 +22,22 @@ 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)$. *)
+(*s Explicit substitutions of type ['a]. *)
 type 'a subs =
-  | ESID of int
-  | CONS of 'a * 'a subs
-  | SHIFT of int * 'a subs
-  | LIFT of int * 'a subs
+  | ESID of int            (* ESID(n)    = %n END   bounded identity *)
+  | CONS of 'a array * 'a subs
+                           (* CONS([|t1..tn|],S)  =
+                              (S.t1...tn)    parallel substitution
+                              beware of the order *)
+  | 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) *)
 
-val subs_cons: 'a * 'a subs -> 'a subs
+val subs_cons: 'a array * '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 subs_shift_cons: int * 'a subs * 'a array -> 'a subs
 val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
 val is_subs_id: 'a subs -> bool
-val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
\ No newline at end of file
+val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0e7c819b6..fbb06940d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -724,7 +724,7 @@ let check_one_fix renv recpos def =
       | Const kn -> 
           if evaluable_constant kn renv.env then 
             try List.for_all (check_rec_call renv) l
-            with (FixGuardError _ ) as e ->
+            with (FixGuardError _ ) ->
 	      check_rec_call renv(applist(constant_value renv.env kn, l))
 	  else List.for_all (check_rec_call renv) l
 
diff --git a/kernel/term.ml b/kernel/term.ml
index b082c091e..87c319a1b 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -752,19 +752,17 @@ let rec lift_substituend depth s =
 
 let make_substituend c = { sinfo=Unknown; sit=c }
 
-let substn_many lamv n =
+let substn_many lamv n c =
   let lv = Array.length lamv in 
-  let rec substrec depth c = match kind_of_term c with
-    | Rel k     ->
-        if k<=depth then 
-	  c
-        else if k-depth <= lv then
-          lift_substituend depth lamv.(k-depth-1)
-        else 
-	  mkRel (k-lv)
-    | _ -> map_constr_with_binders succ substrec depth c
-  in 
-  substrec n
+  if lv = 0 then c
+  else 
+    let rec substrec depth c = match kind_of_term c with
+      | Rel k     ->
+          if k<=depth then c
+          else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
+          else mkRel (k-lv)
+      | _ -> map_constr_with_binders succ substrec depth c in 
+    substrec n c
 
 (*
 let substkey = Profile.declare_profile "substn_many";;
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 8042bff54..61c11b6d4 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -45,10 +45,10 @@ open Esubst
  *)
 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 constructor * cbv_value list
+  | LAM of int * (name * constr) list * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value array
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value array
+  | CONSTR of constructor * cbv_value array
 
 (* les vars pourraient etre des constr,
    cela permet de retarder les lift: utile ?? *) 
@@ -58,13 +58,13 @@ type cbv_value =
  *)
 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))
+  | LAM (n,ctxt,b,s) -> LAM (n,ctxt,b,subs_shft (n,s))
   | FIXP (fix,s,args) ->
-      FIXP (fix,subs_shft (n,s), List.map (shift_value n) args)
+      FIXP (fix,subs_shft (n,s), Array.map (shift_value n) args)
   | COFIXP (cofix,s,args) ->
-      COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args)
+      COFIXP (cofix,subs_shft (n,s), Array.map (shift_value n) args)
   | CONSTR (c,args) ->
-      CONSTR (c, List.map (shift_value n) args)
+      CONSTR (c, Array.map (shift_value n) args)
 	
 
 (* Contracts a fixpoint: given a fixpoint and a bindings,
@@ -74,22 +74,14 @@ let rec shift_value n = function
  *    -> (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 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)
+  subs_cons(Array.init n make_body, env), bds.(i)
 
 let contract_cofixp env (i,(_,_,bds as bodies)) =
-  let make_body j = COFIXP((j,bodies), env, []) in
+  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)
+  subs_cons(Array.init n make_body, env), bds.(i)
 
 let make_constr_ref n = function
   | RelKey p -> mkRel (n+p)
@@ -99,9 +91,11 @@ let make_constr_ref n = function
 
 (* 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
+ *   APP(v,stk) means the term is applied to v, and then the context stk
+ *      (v.0 is the first argument).
  *      this corresponds to the application stack of the KAM.
- *      The members of l are values: we evaluate arguments before the function.
+ *      The members of l are values: we evaluate arguments before
+        calling 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
@@ -114,15 +108,15 @@ let make_constr_ref n = function
 
 type cbv_stack =
   | TOP
-  | APP of cbv_value list * cbv_stack
+  | APP of cbv_value array * 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)
+  if Array.length appl = 0 then stack else
+    match stack with
+    | APP(args,stk) -> APP(Array.append appl args,stk)
+    | _             -> APP(appl, stack)
 
 
 open RedFlags
@@ -137,23 +131,21 @@ let red_set_ref flags = function
  *)
 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 (c,app) -> (CONSTR(c,[]), stack_app app stack)
+    | FIXP (fix,env,app) -> (FIXP(fix,env,[||]), stack_app app stack)
+    | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[||]), stack_app app stack)
+    | CONSTR (c,app) -> (CONSTR(c,[||]), stack_app app stack)
     | _ -> (head, stack)
 
 
-(* Tests if fixpoint reduction is possible. A reduction function is given as
-   argument *)
-let rec check_app_constr = function
-  | ([], _) -> false
-  | ((CONSTR _)::_, 0) -> true
-  | (_::l, n) -> check_app_constr (l,(pred n))
-	
+(* Tests if fixpoint reduction is possible. *)
 let fixp_reducible flgs ((reci,i),_) stk =
   if red_set flgs fIOTA then
-    match stk with               (* !!! for Acc_rec: reci.(i) = -2 *)
-      | APP(appl,_) -> reci.(i) >=0 & check_app_constr (appl, reci.(i))
+    match stk with
+      | APP(appl,_) ->
+          Array.length appl > reci.(i) &&
+          (match appl.(reci.(i)) with
+              CONSTR _ -> true
+            | _ -> false)
       | _ -> false
   else 
     false
@@ -166,6 +158,7 @@ let cofixp_reducible flgs _ stk =
   else 
     false
 
+
 (* The main recursive functions
  *
  * Go under applications and cases (pushed in the stack), expand head
@@ -184,7 +177,7 @@ let rec norm_head info env t stack =
   | App (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)
+      norm_head info env head (stack_app nargs stack)
   | Case (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack))
   | Cast (ct,_,_) -> norm_head info env ct stack
 
@@ -212,7 +205,7 @@ let rec norm_head info env t stack =
           or red_set (info_flags info) fDELTA
           *)
         then 
-	  subs_cons (cbv_stack_term info TOP env b,env)
+	  subs_cons ([|cbv_stack_term info TOP env b|],env)
 	else
 	  subs_lift env in
       if zeta then
@@ -225,10 +218,12 @@ let rec norm_head info env t stack =
 	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
 
   (* non-neutral cases *)
-  | Lambda (x,a,b) -> (LAM(x,a,b,env), stack)
-  | Fix fix -> (FIXP(fix,env,[]), stack)
-  | CoFix cofix -> (COFIXP(cofix,env,[]), stack)
-  | Construct c -> (CONSTR(c, []), stack)
+  | Lambda _ ->
+      let ctxt,b = decompose_lam t in
+      (LAM(List.length ctxt, ctxt,b,env), stack)
+  | Fix fix -> (FIXP(fix,env,[||]), stack)
+  | CoFix cofix -> (COFIXP(cofix,env,[||]), stack)
+  | Construct c -> (CONSTR(c, [||]), stack)
 
   (* neutral cases *)
   | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack)
@@ -253,10 +248,18 @@ and norm_head_ref k info env stack normt =
 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))
+    | (LAM (nlams,ctxt,b,env), APP (args, stk))
       when red_set (info_flags info) fBETA ->
-        let subs = subs_cons (arg,env) in
-          cbv_stack_term info (stack_app args stk) subs b
+        let nargs = Array.length args in
+        if nargs == nlams then
+          cbv_stack_term info stk (subs_cons(args,env)) b
+        else if nlams < nargs then
+          let env' = subs_cons(Array.sub args 0 nlams, env) in
+          let eargs = Array.sub args nlams (nargs-nlams) in
+          cbv_stack_term info (APP(eargs,stk)) env' b
+        else
+          let (_,ctxt') = list_chop nargs ctxt in
+          LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,_), stk)
@@ -273,8 +276,9 @@ and cbv_stack_term info stack env t =
     (* constructor in a Case -> IOTA *)
     | (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk)))
             when red_set (info_flags info) fIOTA ->
-	let real_args = list_skipn ci.ci_npar args in
-        cbv_stack_term info (stack_app real_args stk) env br.(n-1)
+	let cargs =
+          Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
+        cbv_stack_term info (stack_app cargs stk) env br.(n-1)
          
     (* constructor of arity 0 in a Case -> IOTA *)
     | (CONSTR((_,n),_), CASE(_,br,_,env,stk))
@@ -287,6 +291,9 @@ and cbv_stack_term info stack env t =
     | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) 
     | (CONSTR(c,_), APP(appl,TOP)) -> CONSTR(c,appl)
 
+    (* absurd cases (ill-typed) *)
+    | (LAM _, CASE _) -> assert false
+
     (* definitely a value *)
     | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
 
@@ -298,7 +305,7 @@ and cbv_stack_term info stack env t =
 and apply_stack info t = function
   | TOP -> t
   | APP (args,st) ->
-      apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st
+      apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st
   | CASE (ty,br,ci,env,st) ->
       apply_stack info
         (mkCase (ci, cbv_norm_term info env ty, t,
@@ -314,28 +321,28 @@ and cbv_norm_term info 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)
+  | LAM (n,ctxt,b,env) ->
+      let nctxt =
+        list_map_i (fun i (x,ty) ->
+          (x,cbv_norm_term info (subs_liftn (n-i) env) ty)) 0 ctxt in
+      compose_lam nctxt (cbv_norm_term info (subs_liftn n env) b)
   | FIXP ((lij,(names,lty,bds)),env,args) ->
-      applistc
+      mkApp
         (mkFix (lij,
 		(names,
                  Array.map (cbv_norm_term info env) lty,
 		 Array.map (cbv_norm_term info 
-			      (subs_liftn (Array.length lty) env)) bds)))
-        (List.map (cbv_norm_value info) args)
+			      (subs_liftn (Array.length lty) env)) bds)),
+         Array.map (cbv_norm_value info) args)
   | COFIXP ((j,(names,lty,bds)),env,args) ->
-      applistc
+      mkApp
         (mkCoFix (j,
 		  (names,Array.map (cbv_norm_term info env) lty,
 		   Array.map (cbv_norm_term info 
-				(subs_liftn (Array.length lty) env)) bds)))
-        (List.map (cbv_norm_value info) args)
+				(subs_liftn (Array.length lty) env)) bds)),
+         Array.map (cbv_norm_value info) args)
   | CONSTR (c,args) ->
-      applistc
-        (mkConstruct c)
-        (List.map (cbv_norm_value info) args)
+      mkApp(mkConstruct c, Array.map (cbv_norm_value info) args)
 
 (* with profiling *)
 let cbv_norm infos constr =
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 0eb5ce9bf..21b65a57e 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -29,19 +29,19 @@ val cbv_norm         : 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 constructor * cbv_value list
+  | LAM of int * (name * constr) list * constr * cbv_value subs
+  | FIXP of fixpoint * cbv_value subs * cbv_value array
+  | COFIXP of cofixpoint * cbv_value subs * cbv_value array
+  | CONSTR of constructor * cbv_value array
 
 val shift_value : int -> cbv_value -> cbv_value
 
 type cbv_stack =
   | TOP
-  | APP of cbv_value list * cbv_stack
+  | APP of cbv_value array * 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 stack_app : cbv_value array -> cbv_stack -> cbv_stack
 val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
 (* recursive functions... *)