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

1 files changed, 0 insertions, 11 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index ccbfbc4c0..591b353db 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -496,9 +496,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
   | [] -> []
@@ -547,8 +544,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
@@ -857,12 +852,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 ->