From f8b5525eea31c226dfb2ebdc22be512f8af2ebbe Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 8 Apr 2009 17:23:13 +0000
Subject: Some dead code removal + cleanups

  This commit concerns about the first half of the useless code
  mentionned by Oug for coqtop (without plugins). For the moment,
  Oug is used in a mode where any elements mentionned in a .mli
  is considered to be precious. This already allows to detect and
  remove about 600 lines, and more is still to come.

  Among the interesting points, the type Entries.specification_entry
  and its constructors SPExxx were never used. Large parts of cases.ml
  (and hence subtac_cases.ml) were also useless.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.ml | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'kernel/closure.ml')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 10ef06993a..c4759fa925 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -379,9 +379,6 @@ let rec decomp_stack = function
         | _ ->
             Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
   | _ -> None
-let rec decomp_stackn = function
-  | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s)
-  | _ -> assert false
 let array_of_stack s =
   let rec stackrec = function
   | [] -> []
@@ -430,8 +427,6 @@ 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 lift_fconstr_list k l =
-  if k=0 then l else List.map (fun f -> lft_fconstr k f) l
 
 let clos_rel e i =
   match expand_rel i e with
@@ -741,12 +736,6 @@ let get_nth_arg head 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  decomp_stack stk' with
-      Some (v, s') -> (Some (depth,v), s')
-    | None -> (None, zshift depth stk')
-
 let rec get_args n tys f e stk =
   match stk with
       Zupdate r :: s ->
-- 
cgit v1.2.3