From 4ea9567b49be0582a5b2420646e5036b60aedd72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 23 Dec 2018 15:17:31 +0100
Subject: Remove dead code from CClosure.

It seems that it was a remnant of a time where Reductionops would share the
same data types.
---
 kernel/cClosure.ml  | 40 ----------------------------------------
 kernel/cClosure.mli |  9 +--------
 2 files changed, 1 insertion(+), 48 deletions(-)

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1f61bcae2e..196bb16f32 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -374,46 +374,6 @@ let rec stack_args_size = function
   | Zupdate(_)::s -> stack_args_size s
   | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0
 
-(* When used as an argument stack (only Zapp can appear) *)
-let rec decomp_stack = function
-  | Zapp v :: s ->
-      (match Array.length v with
-          0 -> decomp_stack s
-        | 1 -> Some (v.(0), s)
-        | _ ->
-            Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
-  | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> None
-let array_of_stack s =
-  let rec stackrec = function
-  | [] -> []
-  | Zapp args :: s -> args :: (stackrec s)
-  | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ -> assert false
-  in Array.concat (stackrec s)
-let rec stack_assign s p c = match s with
-  | Zapp args :: s ->
-      let q = Array.length args in
-      if p >= q then
-	Zapp args :: stack_assign s (p-q) c
-      else
-        (let nargs = Array.copy args in
-         nargs.(p) <- c;
-         Zapp nargs :: s)
-  | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> s
-let rec stack_tail p s =
-  if Int.equal p 0 then s else
-    match s with
-      | Zapp args :: s ->
-	  let q = Array.length args in
-	  if p >= q then stack_tail (p-q) s
-	  else Zapp (Array.sub args p (q-p)) :: s
-      | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> failwith "stack_tail"
-let rec stack_nth s p = match s with
-  | Zapp args :: s ->
-      let q = Array.length args in
-      if p >= q then stack_nth s (p-q)
-      else args.(p)
-  | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> raise Not_found
-
 (* Lifting. Preserves sharing (useful only for cell with norm=Red).
    lft_fconstr always create a new cell, while lift_fconstr avoids it
    when the lift is 0. *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index c2d53eed47..46be1bb279 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -123,8 +123,7 @@ type fterm =
 
 (***********************************************************************
   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 *)
+   [append_stack] one array at a time *)
 
 type stack_member =
   | Zapp of fconstr array
@@ -139,13 +138,7 @@ and stack = stack_member list
 val empty_stack : stack
 val append_stack : fconstr array -> stack -> stack
 
-val decomp_stack : stack -> (fconstr * stack) option
-val array_of_stack : stack -> fconstr array
-val stack_assign : stack -> int -> fconstr -> stack
 val stack_args_size : stack -> int
-val stack_tail : int -> stack -> stack
-val stack_nth : stack -> int -> fconstr
-val zip_term : (fconstr -> constr) -> constr -> stack -> constr
 val eta_expand_stack : stack -> stack
 
 (** To lazy reduce a constr, create a [clos_infos] with
-- 
cgit v1.2.3