Stack operations of Reductionops in Reductionops.Stack

8 files changed, 321 insertions, 313 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e1e549eb2..899b64984 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -31,7 +31,7 @@ type flex_kind_of_term =
 let flex_kind_of_term c sk =
   match kind_of_term c with
     | Rel _ | Const _ | Var _ -> MaybeFlexible
-    | Lambda _ when not (Option.is_empty (decomp_stack sk)) -> MaybeFlexible
+    | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible
     | LetIn _  -> MaybeFlexible
     | Evar ev -> Flexible ev
     | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid
@@ -39,9 +39,6 @@ let flex_kind_of_term c sk =
     | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
     | Cast _ | App _ | Case _ -> assert false
 
-let not_purely_applicative_stack args =
-  List.exists (function (Zfix _ | Zcase _) -> true | _ -> false) args
-
 let eval_flexible_term ts env c =
   match kind_of_term c with
   | Const c ->
@@ -63,8 +60,8 @@ let eval_flexible_term ts env c =
 
 let apprec_nohdbeta ts env evd c =
   let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
-  if not_purely_applicative_stack (snd (Reductionops.strip_app sk))
-  then zip (fst (whd_betaiota_deltazeta_for_iota_state
+  if Stack.not_purely_applicative sk
+  then Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state
 		   ts env evd Cst_stack.empty appr))
   else c
 
@@ -100,7 +97,7 @@ let check_conv_record (t1,sk1) (t2,sk2) =
 	match kind_of_term t2 with
 	    Prod (_,a,b) -> (* assert (l2=[]); *)
       	      if dependent (mkRel 1) b then raise Not_found
-	      else lookup_canonical_conversion (proji, Prod_cs),[Zapp [a;pop b]]
+	      else lookup_canonical_conversion (proji, Prod_cs),[Stack.App [a;pop b]]
 	  | Sort s ->
 	      lookup_canonical_conversion
 		(proji, Sort_cs (family_of_sort s)),[]
@@ -113,15 +110,15 @@ let check_conv_record (t1,sk1) (t2,sk2) =
     let { o_DEF = c; o_INJ=n; o_TABS = bs;
           o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
     let params1, c1, extra_args1 =
-      match strip_n_app nparams sk1 with
+      match Stack.strip_n_app nparams sk1 with
 	| Some (params1, c1,extra_args1) -> params1, c1, extra_args1
 	| _ -> raise Not_found in
     let us2,extra_args2 =
-      let l',s' = strip_app sk2_effective in
+      let l',s' = Stack.strip_app sk2_effective in
       let bef,aft = List.chop (List.length us) l' in
-      (bef, append_stack_app_list aft s') in
+      (bef, Stack.append_app_list aft s') in
     c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1,
-    (n,zip(t2,sk2))
+    (n,Stack.zip(t2,sk2))
   with Failure _ | Not_found ->
     raise Not_found
 
@@ -196,14 +193,15 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       else None, x in
     match sk1, sk2 with
     | [], [] -> None, Success i
-    | Zcase (_,t1,c1,_)::q1, Zcase (_,t2,c2,_)::q2 ->
+    | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 ->
       (match f env i CONV t1 t2 with
       | Success i' ->
 	(match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
 	| Success i'' -> ise_stack2 true i'' q1 q2
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
-    | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
+    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
+      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
       if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
         match ise_and i [
 	  (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
@@ -212,9 +210,9 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         | Success i' -> ise_stack2 true i' q1 q2
         | UnifFailure _ as x -> fail x
       else fail (UnifFailure (i,NotSameHead))
-    | Zupdate _ :: _, _ | Zshift _ :: _, _
-    | _, Zupdate _ :: _ | _, Zshift _ :: _ -> assert false
-    | Zapp l1 :: q1, Zapp l2 :: q2 ->
+    | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
+    | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
+    | Stack.App l1 :: q1, Stack.App l2 :: q2 ->
       if no_app&&deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin
       (* Is requiring to match on all the shorter list a restriction
 	 here ? we could imagine a generalization of
@@ -224,15 +222,15 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       match generic_ise_list2 i (fun ii -> f env ii CONV) l1 l2 with
       |_,(UnifFailure _ as x) -> fail x
       |None,Success i' -> ise_stack2 true i' q1 q2
-      |Some (Inl r),Success i' -> ise_stack2 true i' (Zapp r :: q1) q2
-      |Some (Inr r),Success i' -> ise_stack2 true i' q1 (Zapp r :: q2)
+      |Some (Inl r),Success i' -> ise_stack2 true i' (Stack.App r :: q1) q2
+      |Some (Inr r),Success i' -> ise_stack2 true i' q1 (Stack.App r :: q2)
     end
     |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead))
   in ise_stack2 false evd (List.rev sk1) (List.rev sk2)
 
 (* Make sure that the matching suffix is the all stack *)
 let exact_ise_stack2 env evd f sk1 sk2 =
-  if Reductionops.compare_stack_shape sk1 sk2 then
+  if Reductionops.Stack.compare_shape sk1 sk2 then
     ise_exact (ise_stack2 false env evd f) sk1 sk2
   else UnifFailure (evd, (* Dummy *) NotSameHead)
 
@@ -266,17 +264,17 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
             (position_problem false pbty,ev,term1)
         | _ ->
           evar_eqappr_x ts env evd pbty
-            (whd_nored_state evd (term1,empty_stack), Cst_stack.empty)
-            (whd_nored_state evd (term2,empty_stack), Cst_stack.empty)
+            (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
+            (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
         end
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
   let default_fail i = (* costly *)
-    UnifFailure (i,ConversionFailed (env, zip appr1, zip appr2)) in
+    UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in
   let miller_pfenning on_left fallback ev (_,skF) apprM evd =
-    let tM = zip apprM in
-    match list_of_app_stack skF with
+    let tM = Stack.zip apprM in
+    match Stack.list_of_app_stack skF with
     | None -> default_fail evd
     | Some lF -> match is_unification_pattern_evar env evd ev lF tM with
       | None -> fallback ()
@@ -287,18 +285,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  (position_problem on_left pbty,ev,t2) in
   let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) =
     let switch f a b = if on_left then f a b else f b a in
-    let not_only_app = not_purely_applicative_stack skM in
+    let not_only_app = Stack.not_purely_applicative skM in
     let f1 i = miller_pfenning on_left
       (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
-	switch (fun x y -> Success (add_conv_pb (pbty,env,zip x,zip y) i)) apprF apprM
+	switch (fun x y -> Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) i)) apprF apprM
        else default_fail i)
       ev apprF apprM i
     and f2 i =
       match switch (ise_stack2 not_only_app env i (evar_conv_x ts)) skF skM with
       |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (zip(termF,l)) (zip(termM,r))
+	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termM,r))
       |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (zip(termF,l)) (zip(termM,r))
+	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termM,r))
       |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termM
       |_, (UnifFailure _ as x) -> x
       |Some _, _ -> UnifFailure (i,NotSameArgSize)
@@ -316,9 +314,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let c = nf_evar evd c1 in
     let env' = push_rel (na,None,c) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
-      ts env' evd Cst_stack.empty (c'1, empty_stack) in
+      ts env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
-      (zip (term', sk' @ [Zshift 1]), [Zapp [mkRel 1]]), Cst_stack.empty in
+      (Stack.zip (term', sk' @ [Stack.Shift 1]), [Stack.App [mkRel 1]]), Cst_stack.empty in
     if onleft then evar_eqappr_x ts env' evd CONV out1 out2
     else evar_eqappr_x ts env' evd CONV out2 out1
   in
@@ -332,9 +330,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  |None, Success i' -> solve_simple_eqn (evar_conv_x ts) env i'
 	    (position_problem true pbty,ev1,term2)
 	  |Some (r,[]), Success i' -> solve_simple_eqn (evar_conv_x ts) env i'
-	    (position_problem false pbty,ev2,zip(term1,r))
+	    (position_problem false pbty,ev2,Stack.zip(term1,r))
 	  |Some ([],r), Success i' -> solve_simple_eqn (evar_conv_x ts) env i'
-	          (position_problem true pbty,ev1,zip(term2,r))
+	          (position_problem true pbty,ev1,Stack.zip(term2,r))
 	  |_, (UnifFailure _ as x) -> x
 	  |Some _, _ -> UnifFailure (i,NotSameArgSize)
 	and f2 i =
@@ -390,9 +388,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
              usable as a canonical projection or canonical value *)
           let rec is_unnamed (hd, args) = match kind_of_term hd with
             | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) ->
-	      not_purely_applicative_stack args
+	      Stack.not_purely_applicative args
             | (CoFix _|Meta _|Rel _)-> true
-            | Evar _ -> not_purely_applicative_stack args
+            | Evar _ -> Stack.not_purely_applicative args
 	    (* false (* immediate solution without Canon Struct *)*)
             | Lambda _ -> assert (match args with [] -> true | _ -> false); true
             | LetIn (_,b,_,c) -> is_unnamed
@@ -403,14 +401,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             match eval_flexible_term ts env term2 with
             | None -> false
             | Some v2 ->
-	      let applicative_stack = append_stack_app_list (fst (strip_app sk2)) empty_stack in
+	      let applicative_stack = Stack.append_app_list (fst (Stack.strip_app sk2)) Stack.empty in
 	      is_unnamed
 		(fst (whd_betaiota_deltazeta_for_iota_state
 			ts env i Cst_stack.empty (v2, applicative_stack))) in
           let rhs_is_already_stuck =
             rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
 	  if (isLambda term1 || rhs_is_already_stuck)
-	    && (not (not_purely_applicative_stack sk1)) then
+	    && (not (Stack.not_purely_applicative sk1)) then
 	    match eval_flexible_term ts env term1 with
 	    | Some v1 ->
 	      evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
@@ -456,7 +454,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       let f1 evd =
 	miller_pfenning true
 	(fun () -> Success ((* Postpone the use of an heuristic *)
-	  add_conv_pb (pbty,env,zip appr1,zip appr2) evd))
+	  add_conv_pb (pbty,env,Stack.zip appr1,Stack.zip appr2) evd))
 	ev1 appr1 appr2 evd
       and f2 evd =
 	if isLambda term2 then
@@ -468,7 +466,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       let f1 evd =
 	miller_pfenning false
 	  (fun () -> Success ((* Postpone the use of an heuristic *)
-	     add_conv_pb (pbty,env,zip appr1,zip appr2) evd))
+	     add_conv_pb (pbty,env,Stack.zip appr1,Stack.zip appr2) evd))
 	ev2 appr2 appr1 evd
       and f2 evd =
 	if isLambda term1 then
@@ -571,7 +569,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with
 	  |_, (UnifFailure _ as x) -> x
 	  |None, Success i' -> evar_conv_x ts env i' CONV term1 term2
-	  |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (zip (term1,sk1')) (zip (term2,sk2'))
+	  |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2'))
 	  end
 
 	| (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _), _ -> UnifFailure (evd,NotSameHead)
@@ -584,7 +582,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       end
 
 and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
-  if Reductionops.compare_stack_shape ts ts1 then
+  if Reductionops.Stack.compare_shape ts ts1 then
     let (evd',ks,_) =
       List.fold_left
 	(fun (i,ks,m) b ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 2a78989f1..65eae6560 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -44,10 +44,10 @@ val check_problems_are_solved : evar_map -> unit
 
 (** Check if a canonical structure is applicable *)
 
-val check_conv_record : constr * types stack -> constr * types stack ->
+val check_conv_record : constr * types Stack.t -> constr * types Stack.t ->
   constr * constr list * (constr list * constr list) *
     (constr list * types list) *
-    (constr stack * types stack) * constr *
+    (constr Stack.t * types Stack.t) * constr *
     (int * constr)
 
 (** Try to solve problems of the form ?x[args] = c by second-order
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fe3606ce4..dfbe9a0b5 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -293,8 +293,8 @@ let is_open_canonical_projection env sigma (c,args) =
   try
     let n = find_projection_nparams (global_of_constr c) in
     try
-      let arg = whd_betadeltaiota env sigma (stack_nth args n) in
+      let arg = whd_betadeltaiota env sigma (Stack.nth args n) in
       let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in
-      not (isConstruct hd) 
+      not (isConstruct hd)
     with Failure _ -> false
   with Not_found -> false
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 062326505..88199c434 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -70,6 +70,6 @@ val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
 val declare_canonical_structure : global_reference -> unit
 val is_open_canonical_projection :
-  Environ.env -> Evd.evar_map -> (constr * constr Reductionops.stack) -> bool
+  Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool
 val canonical_projections : unit ->
   ((global_reference * cs_pattern) * obj_typ) list
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 98fc8f055..32c57694b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -16,8 +16,6 @@ open Termops
 open Univ
 open Evd
 open Environ
-open Closure
-open Reduction
 
 exception Elimconst
 
@@ -30,150 +28,156 @@ exception Elimconst
 
 
 (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
-type 'a stack_member =
-  | Zapp of 'a list
-  | Zcase of case_info * 'a * 'a array * ('a * 'a list) option
-  | Zfix of fixpoint * 'a stack * ('a * 'a list) option
-  | Zshift of int
-  | Zupdate of 'a
-and 'a stack = 'a stack_member list
-
-let compare_stack_shape stk1 stk2 =
-  let rec compare_rec bal stk1 stk2 =
-  match (stk1,stk2) with
-      ([],[]) -> Int.equal bal 0
-    | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
-    | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
-    | (Zapp l1::s1, _) -> compare_rec (bal+List.length l1) s1 stk2
-    | (_, Zapp l2::s2) -> compare_rec (bal-List.length l2) stk1 s2
-    | (Zcase(c1,_,_,_)::s1, Zcase(c2,_,_,_)::s2) ->
+module Stack = struct
+  type 'a member =
+  | App of 'a list
+  | Case of case_info * 'a * 'a array * ('a * 'a list) option
+  | Fix of fixpoint * 'a t * ('a * 'a list) option
+  | Shift of int
+  | Update of 'a
+  and 'a t = 'a member list
+
+  let compare_shape stk1 stk2 =
+    let rec compare_rec bal stk1 stk2 =
+      match (stk1,stk2) with
+	([],[]) -> Int.equal bal 0
+      | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2
+      | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2
+      | (App l1::s1, _) -> compare_rec (bal+List.length l1) s1 stk2
+      | (_, App l2::s2) -> compare_rec (bal-List.length l2) stk1 s2
+      | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
-    | (Zfix(_,a1,_)::s1, Zfix(_,a2,_)::s2) ->
+      | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
-    | (_,_) -> false in
-  compare_rec 0 stk1 stk2
+      | (_,_) -> false in
+    compare_rec 0 stk1 stk2
+
+  let fold2 f o sk1 sk2 =
+    let rec aux o lft1 sk1 lft2 sk2 =
+      let fold_array =
+	Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y))
+      in
+      match sk1,sk2 with
+      | [], [] -> o,lft1,lft2
+      | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2
+      | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2
+      | App [] :: q1, _ -> aux o lft1 q1 lft2 sk2
+      | _, App [] :: q2 -> aux o lft1 sk1 lft2 q2
+      | App (t1::l1) :: q1, App (t2::l2) :: q2 ->
+	aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
+	  lft1 (App l1 :: q1) lft2 (App l2 :: q2)
+      | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 ->
+	aux (fold_array
+	       (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
+	       a1 a2) lft1 q1 lft2 q2
+      | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 ->
+	let (o',_,_) = aux (fold_array (fold_array o b1 b2) a1 a2)
+	  lft1 s1 lft2 s2 in
+	aux o' lft1 q1 lft2 q2
+      | _, _ -> raise (Invalid_argument "Reductionops.Stack.fold2")
+    in aux o 0 (List.rev sk1) 0 (List.rev sk2)
 
-let fold_stack2 f o sk1 sk2 =
-  let rec aux o lft1 sk1 lft2 sk2 =
-  let fold_array =
-    Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y))
-  in
-  match sk1,sk2 with
-  | [], [] -> o,lft1,lft2
-  | Zshift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2
-  | _, Zshift n :: q2 -> aux o lft1 sk1 (lft2+n) q2
-  | Zapp [] :: q1, _ -> aux o lft1 q1 lft2 sk2
-  | _, Zapp [] :: q2 -> aux o lft1 sk1 lft2 q2
-  | Zapp (t1::l1) :: q1, Zapp (t2::l2) :: q2 ->
-    aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
-      lft1 (Zapp l1 :: q1) lft2 (Zapp l2 :: q2)
-  | Zcase (_,t1,a1,_) :: q1, Zcase (_,t2,a2,_) :: q2 ->
-    aux (fold_array
-	   (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
-	   a1 a2) lft1 q1 lft2 q2
-  | Zfix ((_,(_,a1,b1)),s1,_) :: q1, Zfix ((_,(_,a2,b2)),s2,_) :: q2 ->
-    let (o',_,_) = aux (fold_array (fold_array o b1 b2) a1 a2)
-      lft1 s1 lft2 s2 in
-    aux o' lft1 q1 lft2 q2
-  | _, _ -> raise (Invalid_argument "Reductionops.fold_stack2")
-  in aux o 0 (List.rev sk1) 0 (List.rev sk2)
-
-let empty_stack = []
-let append_stack_app_list l s =
-  match (l,s) with
-  | ([],s) -> s
-  | (l1, Zapp l :: s) -> Zapp (l1@l) :: s
-  | (l1, s) -> Zapp l1 :: s
-
-let append_stack_app v s =
-  if Array.is_empty v then s
-  else match s with
-  | Zapp l :: s ->
-    let rec append i accu =
-      if i < 0 then accu
-      else
-        let arg = Array.unsafe_get v i in
-        append (pred i) (arg :: accu)
-    in
-    let al = append (Array.length v - 1) l in
-    Zapp al :: s
-  | _ -> Zapp (Array.to_list v) :: s
-
-let rec stack_args_size = function
-  | Zapp l::s -> List.length l + stack_args_size s
-  | Zshift(_)::s -> stack_args_size s
-  | Zupdate(_)::s -> stack_args_size s
-  | _ -> 0
-
-let rec decomp_stack = function
-  | Zapp[v]::s -> Some (v, s)
-  | Zapp(v::l)::s -> Some (v, (Zapp l :: s))
-  | Zapp [] :: s -> decomp_stack s
-  | _ -> None
-let rec strip_app = function
-  | Zapp args :: s -> let (args',s') = strip_app s in args @ args', s'
-  | s -> [],s
-let strip_n_app n s =
-  let apps,s' = strip_app s in
-  try
-    let bef,aft = List.chop n apps in
-    match aft with
+  let empty = []
+  let append_app_list l s =
+    match (l,s) with
+    | ([],s) -> s
+    | (l1, App l :: s) -> App (l1@l) :: s
+    | (l1, s) -> App l1 :: s
+
+  let append_app v s =
+    if Array.is_empty v then s
+    else match s with
+    | App l :: s ->
+      let rec append i accu =
+	if i < 0 then accu
+	else
+          let arg = Array.unsafe_get v i in
+          append (pred i) (arg :: accu)
+      in
+      let al = append (Array.length v - 1) l in
+      App al :: s
+    | _ -> App (Array.to_list v) :: s
+
+  let rec args_size = function
+    | App l::s -> List.length l + args_size s
+    | Shift(_)::s -> args_size s
+    | Update(_)::s -> args_size s
+    | _ -> 0
+
+  let rec decomp = function
+    | App[v]::s -> Some (v, s)
+    | App(v::l)::s -> Some (v, (App l :: s))
+    | App [] :: s -> decomp s
+    | _ -> None
+  let rec strip_app = function
+    | App args :: s -> let (args',s') = strip_app s in args @ args', s'
+    | s -> [],s
+  let strip_n_app n s =
+    let apps,s' = strip_app s in
+    try
+      let bef,aft = List.chop n apps in
+      match aft with
       |h::[] -> Some (bef,h,s')
-      |h::t -> Some (bef,h,append_stack_app_list t s')
+      |h::t -> Some (bef,h,append_app_list t s')
       |[] -> None
-  with
+    with
     |Failure _ -> None
-let nfirsts_app_of_stack n s =
-  let (args, _) = strip_app s in List.firstn n args
-let list_of_app_stack s =
-  let (out,s') = strip_app s in
-  let init = match s' with [] -> true | _ -> false in
-  Option.init init out
-let array_of_app_stack s =
-  Option.map Array.of_list (list_of_app_stack s)
-let rec stack_assign s p c = match s with
-  | Zapp args :: s ->
+  let nfirsts_app n s =
+    let (args, _) = strip_app s in List.firstn n args
+
+  let not_purely_applicative args =
+    List.exists (function (Fix _ | Case _) -> true | _ -> false) args
+  let list_of_app_stack s =
+    let (out,s') = strip_app s in
+    let init = match s' with [] -> true | _ -> false in
+    Option.init init out
+  let array_of_app_stack s =
+    Option.map Array.of_list (list_of_app_stack s)
+
+  let rec assign s p c = match s with
+    | App args :: s ->
       let q = List.length args in
       if p >= q then
-	Zapp args :: stack_assign s (p-q) c
+	App args :: assign s (p-q) c
       else
         (match List.chop p args with
-            (bef, _::aft) -> Zapp (bef@c::aft) :: s
-          | _ -> assert false)
-  | _ -> s
-let rec stack_tail p s =
-  if Int.equal p 0 then s else
-    match s with
-      | Zapp args :: s ->
-	  let q = List.length args in
-	  if p >= q then stack_tail (p-q) s
-	  else Zapp (List.skipn p args) :: s
-      | _ -> failwith "stack_tail"
-let rec stack_nth s p = match s with
-  | Zapp args :: s ->
+          (bef, _::aft) -> App (bef@c::aft) :: s
+        | _ -> assert false)
+    | _ -> s
+  let rec tail p s =
+    if Int.equal p 0 then s else
+      match s with
+      | App args :: s ->
+	let q = List.length args in
+	if p >= q then tail (p-q) s
+	else App (List.skipn p args) :: s
+      | _ -> failwith "Reductionops.Stack.tail"
+  let rec nth s p = match s with
+    | App args :: s ->
       let q = List.length args in
-      if p >= q then stack_nth s (p-q)
+      if p >= q then nth s (p-q)
       else List.nth args p
-  | _ -> raise Not_found
-
-let rec zip ?(refold=false) = function
-  | f, [] -> f
-  | f, (Zapp [] :: s) -> zip ~refold (f, s)
-  | f, (Zapp args :: s) ->
-      zip ~refold (applist (f, args), s)
-  | f, (Zcase (ci,rt,br,Some(cst, params))::s) when refold ->
-    zip ~refold (cst, append_stack_app_list (List.rev params) s)
-  | f, (Zcase (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s)
-  | f, (Zfix (fix,st,Some(cst, params))::s) when refold -> zip ~refold
-    (cst, append_stack_app_list (List.rev params)
-      (st @ (append_stack_app_list [f] s)))
-  | f, (Zfix (fix,st,_)::s) -> zip ~refold
-    (mkFix fix, st @ (append_stack_app_list [f] s))
-  | f, (Zshift n::s) -> zip ~refold (lift n f, s)
+    | _ -> raise Not_found
+
+  let rec zip ?(refold=false) = function
+    | f, [] -> f
+    | f, (App [] :: s) -> zip ~refold (f, s)
+    | f, (App args :: s) ->
+       zip ~refold (applist (f, args), s)
+    | f, (Case (ci,rt,br,Some(cst, params))::s) when refold ->
+       zip ~refold (cst, append_app_list (List.rev params) s)
+    | f, (Case (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s)
+    | f, (Fix (fix,st,Some(cst, params))::s) when refold ->
+       zip ~refold (cst, append_app_list (List.rev params)
+      (st @ (append_app_list [f] s)))
+  | f, (Fix (fix,st,_)::s) -> zip ~refold
+    (mkFix fix, st @ (append_app_list [f] s))
+  | f, (Shift n::s) -> zip ~refold (lift n f, s)
   | _ -> assert false
+end
 
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
-type state = constr * constr stack
+type state = constr * constr Stack.t
 
 type  contextual_reduction_function = env ->  evar_map -> constr -> constr
 type  reduction_function =  contextual_reduction_function
@@ -272,7 +276,7 @@ end
 
 let apply_subst recfun env cst_l t stack =
   let rec aux env cst_l t stack =
-    match (decomp_stack stack,kind_of_term t) with
+    match (Stack.decomp stack,kind_of_term t) with
     | Some (h,stacktl), Lambda (_,_,c) ->
       aux (h::env) (Cst_stack.add_param h cst_l) c stacktl
     | _ -> recfun cst_l (substl env t, stack)
@@ -282,7 +286,7 @@ let rec stacklam recfun env t stack =
 apply_subst (fun _ -> recfun) env [] t stack
 
 let beta_applist (c,l) =
-  stacklam zip [] c (append_stack_app_list l empty_stack)
+  stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty)
 
 (* Iota reduction tools *)
 
@@ -367,7 +371,7 @@ let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum && bodynum < Array.length recindices);
   let recargnum = Array.get recindices bodynum in
   try
-    Some (recargnum, stack_nth stack recargnum)
+    Some (recargnum, Stack.nth stack recargnum)
   with Not_found ->
     None
 
@@ -384,10 +388,10 @@ let rec whd_state_gen ?csts refold flags env sigma =
   let noth = [] in
   let rec whrec cst_l (x, stack as s) =
     let best_state def (cst,params,nb_skip) =
-      let apps,s' = strip_app stack in
+      let apps,s' = Stack.strip_app stack in
       try
 	let _,aft = List.chop nb_skip apps in
-	(cst, append_stack_app_list (List.rev params) (append_stack_app_list aft s'))
+	(cst, Stack.append_app_list (List.rev params) (Stack.append_app_list aft s'))
       with Failure _ -> def in
     let fold () =
       if refold then (List.fold_left best_state s cst_l,noth) else (s,cst_l)
@@ -419,53 +423,54 @@ let rec whd_state_gen ?csts refold flags env sigma =
     | App (f,cl)  ->
       whrec
 	(Cst_stack.add_args cl cst_l)
-	(f, append_stack_app cl stack)
+	(f, Stack.append_app cl stack)
     | Lambda (na,t,c) ->
-      (match decomp_stack stack with
+      (match Stack.decomp stack with
       | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
 	apply_subst whrec [] cst_l x stack
       | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
 	let env' = push_rel (na,None,t) env in
 	let whrec' = whd_state_gen refold flags env' sigma in
-        (match kind_of_term (zip ~refold (fst (whrec' (c, empty_stack)))) with
+        (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with
         | App (f,cl) ->
 	  let napp = Array.length cl in
 	  if napp > 0 then
-	    let (x', l'),_ = whrec' (Array.last cl, empty_stack) in
+	    let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in
             match kind_of_term x', l' with
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop u,empty_stack),noth else fold ()
+	      if noccurn 1 u then (pop u,Stack.empty),noth else fold ()
             | _ -> fold ()
 	  else fold ()
 	| _ -> fold ())
       | _ -> fold ())
 
     | Case (ci,p,d,lf) ->
-      whrec noth (d, Zcase (ci,p,lf,Cst_stack.best_cst cst_l) :: stack)
+      whrec noth (d, Stack.Case (ci,p,lf,Cst_stack.best_cst cst_l) :: stack)
 
     | Fix ((ri,n),_ as f) ->
-      (match strip_n_app ri.(n) stack with
+      (match Stack.strip_n_app ri.(n) stack with
       |None -> fold ()
-      |Some (bef,arg,s') -> whrec noth (arg, Zfix(f,[Zapp bef],Cst_stack.best_cst cst_l)::s'))
+      |Some (bef,arg,s') ->
+	whrec noth (arg, Stack.Fix(f,[Stack.App bef],Cst_stack.best_cst cst_l)::s'))
 
     | Construct (ind,c) ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
-	match strip_app stack with
-	|args, (Zcase(ci, _, lf,_)::s') ->
-	  whrec noth (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	|args, (Zfix (f,s',cst)::s'') ->
+	match Stack.strip_app stack with
+	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	  whrec noth (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	|args, (Stack.Fix (f,s',cst)::s'') ->
 	  let x' = applist(x,args) in
 	  whrec noth ((if refold then contract_fix ~env f else contract_fix f) cst,
-		      s' @ (append_stack_app_list [x'] s''))
+		      s' @ (Stack.append_app_list [x'] s''))
 	|_ -> fold ()
       else fold ()
 
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
-	match strip_app stack with
-	|args, (Zcase(ci, _, lf,_)::s') ->
+	match Stack.strip_app stack with
+	|args, (Stack.Case(ci, _, lf,_)::s') ->
 	  whrec noth ((if refold
 	    then contract_cofix ~env cofix
 	    else contract_cofix cofix) (Cst_stack.best_cst cst_l), stack)
@@ -484,34 +489,34 @@ let local_whd_state_gen flags sigma =
     | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA ->
       stacklam whrec [b] c stack
     | Cast (c,_,_) -> whrec (c, stack)
-    | App (f,cl)  -> whrec (f, append_stack_app cl stack)
+    | App (f,cl)  -> whrec (f, Stack.append_app cl stack)
     | Lambda (_,_,c) ->
-      (match decomp_stack stack with
+      (match Stack.decomp stack with
       | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
 	stacklam whrec [a] c m
       | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
-        (match kind_of_term (zip (whrec (c, empty_stack))) with
+        (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with
         | App (f,cl) ->
 	  let napp = Array.length cl in
 	  if napp > 0 then
-	    let x', l' = whrec (Array.last cl, empty_stack) in
+	    let x', l' = whrec (Array.last cl, Stack.empty) in
             match kind_of_term x', l' with
             | Rel 1, [] ->
 	      let lc = Array.sub cl 0 (napp-1) in
 	      let u = if Int.equal napp 1 then f else appvect (f,lc) in
-	      if noccurn 1 u then (pop u,empty_stack) else s
+	      if noccurn 1 u then (pop u,Stack.empty) else s
             | _ -> s
 	  else s
 	| _ -> s)
       | _ -> s)
 
     | Case (ci,p,d,lf) ->
-      whrec (d, Zcase (ci,p,lf,None) :: stack)
+      whrec (d, Stack.Case (ci,p,lf,None) :: stack)
 
     | Fix ((ri,n),_ as f) ->
-      (match strip_n_app ri.(n) stack with
+      (match Stack.strip_n_app ri.(n) stack with
       |None -> s
-      |Some (bef,arg,s') -> whrec (arg, Zfix(f,[Zapp bef],None)::s'))
+      |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,[Stack.App bef],None)::s'))
 
     | Evar ev ->
       (match safe_evar_value sigma ev with
@@ -525,19 +530,19 @@ let local_whd_state_gen flags sigma =
 
     | Construct (ind,c) ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
-	match strip_app stack with
-	|args, (Zcase(ci, _, lf,_)::s') ->
-	  whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	|args, (Zfix (f,s',cst)::s'') ->
+	match Stack.strip_app stack with
+	|args, (Stack.Case(ci, _, lf,_)::s') ->
+	  whrec (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	|args, (Stack.Fix (f,s',cst)::s'') ->
 	  let x' = applist(x,args) in
-	  whrec (contract_fix f cst, s' @ (append_stack_app_list [x'] s''))
+	  whrec (contract_fix f cst, s' @ (Stack.append_app_list [x'] s''))
 	|_ -> s
       else s
 
     | CoFix cofix ->
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
-	match strip_app stack with
-	|args, (Zcase(ci, _, lf,_)::s') ->
+	match Stack.strip_app stack with
+	|args, (Stack.Case(ci, _, lf,_)::s') ->
 	  whrec (contract_cofix cofix None, stack)
 	|_ -> s
       else s
@@ -551,11 +556,11 @@ let raw_whd_state_gen flags env =
   f
 
 let stack_red_of_state_red f =
-  let f sigma x = decompose_app (zip (f sigma (x, empty_stack))) in
+  let f sigma x = decompose_app (Stack.zip (f sigma (x, Stack.empty))) in
   f
 
 let red_of_state_red f sigma x =
-  zip (f sigma (x,empty_stack))
+  Stack.zip (f sigma (x,Stack.empty))
 
 (* 0. No Reduction Functions *)
 
@@ -634,11 +639,11 @@ let whd_betadeltaiota_nolet env =
 
 (* 4. Eta reduction Functions *)
 
-let whd_eta c = zip (local_whd_state_gen eta Evd.empty (c,empty_stack))
+let whd_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty))
 
 (* 5. Zeta Reduction Functions *)
 
-let whd_zeta c = zip (local_whd_state_gen zeta Evd.empty (c,empty_stack))
+let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty))
 
 (****************************************************************************)
 (*                   Reduction Functions                                    *)
@@ -663,9 +668,9 @@ let nf_evar =
 let clos_norm_flags flgs env sigma t =
   try
     let evars ev = safe_evar_value sigma ev in
-    norm_val
-      (create_clos_infos ~evars flgs env)
-      (inject t)
+    Closure.norm_val
+      (Closure.create_clos_infos ~evars flgs env)
+      (Closure.inject t)
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
 let nf_beta = clos_norm_flags Closure.beta empty_env
@@ -682,7 +687,7 @@ let nf_betadeltaiota env sigma =
 *)
 let whd_betaiota_preserving_vm_cast env sigma t =
    let rec stacklam_var subst t stack =
-     match (decomp_stack stack,kind_of_term t) with
+     match (Stack.decomp stack,kind_of_term t) with
      | Some (h,stacktl), Lambda (_,_,c) ->
          begin match kind_of_term h with
          | Rel i when not (evaluable_rel i env) ->
@@ -699,43 +704,43 @@ let whd_betaiota_preserving_vm_cast env sigma t =
               | Some body -> whrec (body, stack)
               | None -> s)
        | Cast (c,VMcast,t) ->
-           let c = zip (whrec (c,empty_stack)) in
-           let t = zip (whrec (t,empty_stack)) in
+           let c = Stack.zip (whrec (c,Stack.empty)) in
+           let t = Stack.zip (whrec (t,Stack.empty)) in
            (mkCast(c,VMcast,t),stack)
        | Cast (c,NATIVEcast,t) ->
-           let c = zip (whrec (c,empty_stack)) in
-           let t = zip (whrec (t,empty_stack)) in
+           let c = Stack.zip (whrec (c,Stack.empty)) in
+           let t = Stack.zip (whrec (t,Stack.empty)) in
            (mkCast(c,NATIVEcast,t),stack)
        | Cast (c,DEFAULTcast,_) ->
            whrec (c, stack)
-       | App (f,cl)  -> whrec (f, append_stack_app cl stack)
+       | App (f,cl)  -> whrec (f, Stack.append_app cl stack)
        | Lambda (na,t,c) ->
-           (match decomp_stack stack with
+           (match Stack.decomp stack with
             | Some (a,m) -> stacklam_var [a] c m
             | _ -> s)
        | Case (ci,p,d,lf) ->
-	 whrec (d, Zcase (ci,p,lf,None) :: stack)
+	 whrec (d, Stack.Case (ci,p,lf,None) :: stack)
 
        | Construct (ind,c) -> begin
-	 match strip_app stack with
-	   |args, (Zcase(ci, _, lf,_)::s') ->
-	     whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	   |args, (Zfix (f,s',cst)::s'') ->
+	 match Stack.strip_app stack with
+	   |args, (Stack.Case(ci, _, lf,_)::s') ->
+	     whrec (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	   |args, (Stack.Fix (f,s',cst)::s'') ->
 	     let x' = applist(x,args) in
-	     whrec (contract_fix f cst,s' @ (append_stack_app_list [x'] s''))
+	     whrec (contract_fix f cst,s' @ (Stack.append_app_list [x'] s''))
 	   |_ -> s
        end
 
        | CoFix cofix -> begin
-	 match strip_app stack with
-	   |args, (Zcase(ci, _, lf,_)::s') ->
+	 match Stack.strip_app stack with
+	   |args, (Stack.Case(ci, _, lf,_)::s') ->
 	     whrec (contract_cofix cofix None, stack)
 	   |_ -> s
        end
 
        | x -> s
    in
-   zip (whrec (t,empty_stack))
+   Stack.zip (whrec (t,Stack.empty))
 
 let nf_betaiota_preserving_vm_cast =
   strong whd_betaiota_preserving_vm_cast
@@ -760,37 +765,37 @@ let is_transparent e k =
 
 type conversion_test = constraints -> constraints
 
-let pb_is_equal pb = pb == CONV
+let pb_is_equal pb = pb == Reduction.CONV
 
 let pb_equal = function
-  | CUMUL -> CONV
-  | CONV -> CONV
+  | Reduction.CUMUL -> Reduction.CONV
+  | Reduction.CONV -> Reduction.CONV
 
-let sort_cmp = sort_cmp
+let sort_cmp = Reduction.sort_cmp
 
 let test_conversion (f: ?l2r:bool-> ?evars:'a->'b) env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
     let _ = f ~evars env x y in
     true
-  with NotConvertible -> false
+  with Reduction.NotConvertible -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
 let is_conv env sigma = test_conversion Reduction.conv env sigma
 let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
-let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
+let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv_leq
 
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
     let _ = f ~evars reds env x y in
     true
-  with NotConvertible -> false
+  with Reduction.NotConvertible -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
 let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv reds env sigma
 let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq reds env sigma
-let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_leq
+let is_trans_fconv = function | Reduction.CONV -> is_trans_conv | Reduction.CUMUL -> is_trans_conv_leq
 
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
@@ -973,14 +978,14 @@ let is_sort env sigma t =
 let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
   let rec whrec csts s =
     let (t, stack as s),csts' = whd_state_gen ~csts false betaiota env sigma s in
-    match strip_app stack with
-      |args, (Zcase _ :: _ as stack') ->
-	let seq = (t,append_stack_app_list args empty_stack) in
+    match Stack.strip_app stack with
+      |args, (Stack.Case _ :: _ as stack') ->
+	let seq = (t,Stack.append_app_list args Stack.empty) in
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
 	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma seq in
 	if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
-      |args, (Zfix _ :: _ as stack') ->
-	let seq = (t,append_stack_app_list args empty_stack) in
+      |args, (Stack.Fix _ :: _ as stack') ->
+	let seq = (t,Stack.append_app_list args Stack.empty) in
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
 	  (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma seq in
 	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
@@ -1001,37 +1006,37 @@ let whd_programs_stack env sigma =
 	  if occur_existential c then
 	    s
 	  else
-	    whrec (mkApp (f, Array.sub cl 0 n), append_stack_app [|c|] stack)
+	    whrec (mkApp (f, Array.sub cl 0 n), Stack.append_app [|c|] stack)
       | LetIn (_,b,_,c) ->
 	  if occur_existential b then
 	    s
 	  else
 	    stacklam whrec [b] c stack
       | Lambda (_,_,c) ->
-          (match decomp_stack stack with
+          (match Stack.decomp stack with
              | None -> s
              | Some (a,m) -> stacklam whrec [a] c m)
       | Case (ci,p,d,lf) ->
 	  if occur_existential d then
 	    s
 	  else
-	    whrec (d, Zcase (ci,p,lf,None) :: stack)
+	    whrec (d, Stack.Case (ci,p,lf,None) :: stack)
       | Fix ((ri,n),_ as f) ->
-	(match strip_n_app ri.(n) stack with
+	(match Stack.strip_n_app ri.(n) stack with
 	  |None -> s
-	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,[Zapp bef],None)::s'))
+	  |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,[Stack.App bef],None)::s'))
       | Construct (ind,c) -> begin
-	match strip_app stack with
-	  |args, (Zcase(ci, _, lf,_)::s') ->
-	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	  |args, (Zfix (f,s',cst)::s'') ->
+	match Stack.strip_app stack with
+	  |args, (Stack.Case(ci, _, lf,_)::s') ->
+	    whrec (lf.(c-1), Stack.append_app_list (List.skipn ci.ci_npar args) s')
+	  |args, (Stack.Fix (f,s',cst)::s'') ->
 	    let x' = applist(x,args) in
-	    whrec (contract_fix f cst,s' @ (append_stack_app_list [x'] s''))
+	    whrec (contract_fix f cst,s' @ (Stack.append_app_list [x'] s''))
 	  |_ -> s
       end
       | CoFix cofix -> begin
-	match strip_app stack with
-	  |args, (Zcase(ci, _, lf,_)::s') ->
+	match Stack.strip_app stack with
+	  |args, (Stack.Case(ci, _, lf,_)::s') ->
 	     whrec (contract_cofix cofix None, stack)
 	  |_ -> s
       end
@@ -1040,7 +1045,7 @@ let whd_programs_stack env sigma =
   whrec
 
 let whd_programs env sigma x =
-  zip (whd_programs_stack env sigma (x, empty_stack))
+  Stack.zip (whd_programs_stack env sigma (x, Stack.empty))
 
 let find_conclusion env sigma =
   let rec decrec env c =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index cd3ed1f2f..7b9eb68d5 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -18,44 +18,49 @@ open Closure
 
 exception Elimconst
 
-(** 90% copy-paste of kernel/closure.ml but polymorphic and with extra
-    arguments for storing refold *)
-type 'a stack_member =
-| Zapp of 'a list
-| Zcase of case_info * 'a * 'a array * ('a * 'a list) option
-| Zfix of fixpoint * 'a stack * ('a * 'a list) option
-| Zshift of int
-| Zupdate of 'a
-
-and 'a stack = 'a stack_member list
-
-val empty_stack : 'a stack
-val compare_stack_shape : 'a stack -> 'a stack -> bool
-(** [fold_stack2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
-@return the result and the lifts to apply on the terms *)
-val fold_stack2 : ('a -> Term.constr -> Term.constr -> 'a) -> 'a ->
-  Term.constr stack -> Term.constr stack -> 'a * int * int
-val append_stack_app : 'a array -> 'a stack -> 'a stack
-val append_stack_app_list : 'a list -> 'a stack -> 'a stack
-
-val decomp_stack : 'a stack -> ('a * 'a stack) option
-val strip_app : 'a stack -> 'a list * 'a stack
-(** Takes the n first arguments of application put on the stack. Fails is the
-    stack does not start by n arguments of application. *)
-val nfirsts_app_of_stack : int -> 'a stack -> 'a list
-(** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
-val strip_n_app : int -> 'a stack -> ('a list * 'a * 'a stack) option
-val list_of_app_stack : 'a stack -> 'a list option
-val array_of_app_stack : 'a stack -> 'a array option
-val stack_assign : 'a stack -> int -> 'a -> 'a stack
-val stack_args_size : 'a stack -> int
-val zip : ?refold:bool -> constr * constr stack -> constr
-val stack_tail : int -> 'a stack -> 'a stack
-val stack_nth : 'a stack -> int -> 'a
+module Stack : sig
+  (** 90% copy-paste of kernel/closure.ml but polymorphic and with extra
+      arguments for storing refold *)
+  type 'a member =
+  | App of 'a list
+  | Case of case_info * 'a * 'a array * ('a * 'a list) option
+  | Fix of fixpoint * 'a t * ('a * 'a list) option
+  | Shift of int
+  | Update of 'a
+  and 'a t = 'a member list
+
+  val empty : 'a t
+  val compare_shape : 'a t -> 'a t -> bool
+  (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
+      @return the result and the lifts to apply on the terms *)
+  val fold2 : ('a -> Term.constr -> Term.constr -> 'a) -> 'a ->
+    Term.constr t -> Term.constr t -> 'a * int * int
+  val append_app : 'a array -> 'a t -> 'a t
+  val append_app_list : 'a list -> 'a t -> 'a t
+
+  val decomp : 'a t -> ('a * 'a t) option
+  val strip_app : 'a t -> 'a list * 'a t
+  (** Takes the n first arguments of application put on the stack. Fails is the
+      stack does not start by n arguments of application. *)
+  val nfirsts_app : int -> 'a t -> 'a list
+  (** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
+  val strip_n_app : int -> 'a t -> ('a list * 'a * 'a t) option
+
+  val not_purely_applicative : 'a t -> bool
+  val list_of_app_stack : 'a t -> 'a list option
+  val array_of_app_stack : 'a t -> 'a array option
+
+  val assign : 'a t -> int -> 'a -> 'a t
+  val args_size : 'a t -> int
+  val tail : int -> 'a t -> 'a t
+  val nth : 'a t -> int -> 'a
+
+  val zip : ?refold:bool -> constr * constr t -> constr
+end
 
 (************************************************************************)
 
-type state = constr * constr stack
+type state = constr * constr Stack.t
 
 type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
@@ -94,7 +99,7 @@ val strong_prodspine : local_reduction_function -> local_reduction_function
 val stack_reduction_of_reduction :
   'a reduction_function -> 'a state_reduction_function
 i*)
-val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a
+val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a
 
 val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds ->
   Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
@@ -201,7 +206,7 @@ val whd_programs :  reduction_function
 
 val contract_fix : ?env:Environ.env -> fixpoint ->
   (constr * constr list) option -> constr
-val fix_recarg : fixpoint -> constr stack -> (int * constr) option
+val fix_recarg : fixpoint -> constr Stack.t -> (int * constr) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
 val is_transparent : Environ.env -> 'a tableKey -> bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index d6ad76f3e..456693a96 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -425,7 +425,7 @@ let substl_checking_arity env subst sigma c =
 type fix_reduction_result = NotReducible | Reduced of (constr*constr list)
 
 let reduce_fix whdfun sigma fix stack =
-  match fix_recarg fix [Zapp stack] with
+  match fix_recarg fix [Stack.App stack] with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') = whdfun sigma recarg in
@@ -442,7 +442,7 @@ let contract_fix_use_function env sigma f
   substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
-  match fix_recarg fix [Zapp stack] with
+  match fix_recarg fix [Stack.App stack] with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
         let (recarg'hd,_ as recarg') =
@@ -626,15 +626,15 @@ let whd_nothing_for_iota env sigma s =
 	     | None -> s)
       | LetIn (_,b,_,c) -> stacklam whrec [b] c stack
       | Cast (c,_,_) -> whrec (c, stack)
-      | App (f,cl)  -> whrec (f, append_stack_app cl stack)
+      | App (f,cl)  -> whrec (f, Stack.append_app cl stack)
       | Lambda (na,t,c) ->
-          (match decomp_stack stack with
+          (match Stack.decomp stack with
              | Some (a,m) -> stacklam whrec [a] c m
 	     | _ -> s)
 
       | x -> s
   in
-  decompose_app (zip (whrec (s,empty_stack)))
+  decompose_app (Stack.zip (whrec (s,Stack.empty)))
 
 (* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
    constants by keeping the name of the constants in the recursive calls;
@@ -764,13 +764,13 @@ let try_red_product env sigma c =
       | App (f,l) ->
           (match kind_of_term f with
              | Fix fix ->
-                 let stack = append_stack_app l empty_stack in
+                 let stack = Stack.append_app l Stack.empty in
                  (match fix_recarg fix stack with
                     | None -> raise Redelimination
                     | Some (recargnum,recarg) ->
                         let recarg' = redrec env recarg in
-                        let stack' = stack_assign stack recargnum recarg' in
-                        simpfun (zip (f,stack')))
+                        let stack' = Stack.assign stack recargnum recarg' in
+                        simpfun (Stack.zip (f,stack')))
              | _ -> simpfun (appvect (redrec env f, l)))
       | Cast (c,_,_) -> redrec env c
       | Prod (x,a,b) -> mkProd (x, a, redrec (push_rel (x,None,a) env) b)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5bb49c1c5..49f12438b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -347,7 +347,7 @@ let oracle_order env cf1 cf2 =
           Some (Conv_oracle.oracle_order (Environ.oracle env) false k1 k2)
 
 let do_reduce ts (env, nb) sigma c =
-  zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, empty_stack)))
+  Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty)))
 
 let use_full_betaiota flags =
   flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
@@ -599,9 +599,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
   and canonical_projections curenvnb pb b cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp cM then
-	let f1l1 = whd_nored_state sigma (cM,empty_stack) in
+	let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
 	  if is_open_canonical_projection env sigma f1l1 then
-	    let f2l2 = whd_nored_state sigma (cN,empty_stack) in
+	    let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
 	      solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -615,9 +615,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       else
 	try f1 () with e when precatchable_exception e ->
 	  if isApp cN then
-	    let f2l2 = whd_nored_state sigma (cN, empty_stack) in
+	    let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
 	      if is_open_canonical_projection env sigma f2l2 then
-		let f1l1 = whd_nored_state sigma (cM, empty_stack) in
+		let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
 		  solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn
 	      else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -627,7 +627,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       try Evarconv.check_conv_record f1l1 f2l2
       with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
     in
-    if Reductionops.compare_stack_shape ts ts1 then
+    if Reductionops.Stack.compare_shape ts ts1 then
       let (evd,ks,_) =
 	List.fold_left
 	  (fun (evd,ks,m) b ->
@@ -645,7 +645,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	(evd,ms,es) us2 us in
       let substn = unilist2 (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
 	substn params1 params in
-	let (substn,_,_) = Reductionops.fold_stack2 (unirec_rec curenvnb pb b false) substn ts ts1 in
+	let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb b false) substn ts ts1 in
         let app = mkApp (c, Array.rev_of_list ks) in
 	unirec_rec curenvnb pb b false substn c1 app
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -971,7 +971,7 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let head_app sigma m =
-  fst (whd_nored_state sigma (m, empty_stack))
+  fst (whd_nored_state sigma (m, Stack.empty))
 
 let check_types env flags (sigma,_,_ as subst) m n =
   if isEvar_or_Meta (head_app sigma m) then