Some dead code removal, thanks to Oug analyzer

 In particular, the unused lib/tlm.ml and lib/gset.ml are removed

 In addition, to simplify code, Libobject.record_object returning only the
 ('a->obj) function, which is enough almost all the time.
 Use Libobject.record_object_full if you really need also the (obj->'a).

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

15 files changed, 2 insertions, 158 deletions

diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 913421087..00f5eb3b0 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -50,12 +50,6 @@ value coq_static_alloc(value size) /* ML */
   return (value) coq_stat_alloc((asize_t) Long_val(size));
 }
 
-value coq_static_free(value blk)  /* ML */
-{
-  coq_stat_free((void *) blk);
-  return Val_unit;
-}
-
 value accumulate_code(value unit) /* ML */
 {
   return (value) accumulate;
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index c0093a49e..79e4d0fea 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -49,7 +49,6 @@ extern code_t accumulate;
 /* functions over global environment */
 
 value coq_static_alloc(value size);  /* ML */
-value coq_static_free(value string); /* ML */
 
 value init_coq_vm(value unit); /* ML */
 value re_init_coq_vm(value unit); /* ML */
diff --git a/kernel/closure.ml b/kernel/closure.ml
index d70ce83a8..6434e1415 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -81,7 +81,6 @@ module type RedFlagsSig = sig
   val red_add_transparent : reds -> transparent_state -> reds
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
-  val red_get_const : reds -> bool * evaluable_global_reference list
 end
 
 module RedFlags = (struct
@@ -156,16 +155,6 @@ module RedFlags = (struct
     | DELTA -> (* Used for Rel/Var defined in context *)
 	incr_cnt red.r_delta delta
 
-  let red_get_const red =
-    let p1,p2 = red.r_const in
-    let (b1,l1) = Idpred.elements p1 in
-    let (b2,l2) = Cpred.elements p2 in
-    if b1=b2 then
-      let l1' = List.map (fun x -> EvalVarRef x) l1 in
-      let l2' = List.map (fun x -> EvalConstRef x) l2 in
-      (b1, l1' @ l2')
-    else error "unrepresentable pair of predicate"
-
 end : RedFlagsSig)
 
 open RedFlags
@@ -690,16 +679,6 @@ let fapp_stack (m,stk) = zip m stk
    (strip_update_shift, through get_arg). *)
 
 (* optimised for the case where there are no shifts... *)
-let strip_update_shift head stk =
-  assert (head.norm <> Red);
-  let rec strip_rec h depth = function
-    | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s
-    | Zupdate(m)::s ->
-        strip_rec (update m (h.norm,h.term)) depth s
-    | stk -> (depth,stk) in
-  strip_rec head 0 stk
-
-(* optimised for the case where there are no shifts... *)
 let strip_update_shift_app head stk =
   assert (head.norm <> Red);
   let rec strip_rec rstk h depth = function
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 4e8b6d2bd..74c91650a 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -60,8 +60,6 @@ module type RedFlagsSig = sig
   (** Tests if a reduction kind is set *)
   val red_set : reds -> red_kind -> bool
 
-  (** Gives the constant list *)
-  val red_get_const : reds -> bool * evaluable_global_reference list
 end
 
 module RedFlags : RedFlagsSig
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 77a322905..983c1f26d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -23,7 +23,6 @@ open Cbytegen
 
 
 external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
-external free_tcode : tcode -> unit = "coq_static_free"
 external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
 
 (*******************)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index c31c6f75d..714da0319 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -69,14 +69,7 @@ type constant_entry =
 
 (*s Modules *)
 
-
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEmodtype of module_struct_entry
-      
-and module_struct_entry = 
+type module_struct_entry =
     MSEident of module_path
   | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 224680dff..2ba306455 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -64,14 +64,7 @@ type constant_entry =
 
 (** {6 Modules } *)
 
-
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEmodtype of module_struct_entry
-
-and module_struct_entry =
+type module_struct_entry =
     MSEident of module_path
   | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 63a7b83ee..e4bf055c9 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -85,15 +85,6 @@ let mind_check_names mie =
   vue since inductive and constructors are not referred to by their
   name, but only by the name of the inductive packet and an index. *)
 
-let mind_check_arities env mie =
-  let check_arity id c =
-    if not (is_arity env c) then
-      raise (InductiveError (NotAnArity id))
-  in
-  List.iter
-    (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar)
-    mie.mind_entry_inds
-
 (************************************************************************)
 (************************************************************************)
 
@@ -549,16 +540,6 @@ let check_positivity kn env_ar params inds =
 (************************************************************************)
 (* Build the inductive packet *)
 
-(* Elimination sorts *)
-let is_recursive = Rtree.is_infinite
-(*  let rec one_is_rec rvec =
-    List.exists (function Mrec(i) -> List.mem i listind
-                   | Imbr(_,lvec) -> array_exists one_is_rec lvec
-                   | Norec -> false) rvec
-  in
-  array_exists one_is_rec
-*)
-
 (* Allowed eliminations *)
 
 let all_sorts = [InProp;InSet;InType]
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 1e2cedee2..289968eb5 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -78,8 +78,6 @@ let instantiate_params full t args sign =
   if rem_args <> [] then fail();
   substl subs ty
 
-let instantiate_partial_params = instantiate_params false
-
 let full_inductive_instantiate mib params sign =
   let dummy = prop_sort in
   let t = mkArity (sign,dummy) in
@@ -95,10 +93,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) =
 
 (* Functions to build standard types related to inductive *)
 
-
-let number_of_inductives mib = Array.length mib.mind_packets
-let number_of_constructors mip = Array.length mip.mind_consnames
-
 (*
 Computing the actual sort of an applied or partially applied inductive type:
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 8b11aa185..452c2e69a 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -54,11 +54,6 @@ type substitution = (module_path * delta_resolver) Umap.t
     
 let empty_subst = Umap.empty
 
-
-let string_of_subst_domain = function
-  | MBI mbid -> debug_string_of_mbid mbid
-  | MPI mp -> string_of_mp mp
-      
 let add_mbid mbid mp resolve =
   Umap.add (MBI mbid) (mp,resolve)
 let add_mp mp1 mp2 resolve =
@@ -109,16 +104,6 @@ let delta_of_mp resolve mp =
       | _ -> anomaly "mod_subst: bad association in delta_resolver"
   with
       Not_found -> mp
-	
-let delta_of_kn resolve kn =
-  try 
-    match Deltamap.find (KN kn) resolve with
-      | Equiv kn1 -> kn1
-      | Inline _ -> kn
-      | _ -> anomaly 
-	  "mod_subst: bad association in delta_resolver"
-  with
-      Not_found -> kn
 
 let remove_mp_delta_resolver resolver mp =
     Deltamap.remove (MP mp) resolver
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e8c831f70..e14e7c900 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -34,13 +34,6 @@ let rec list_split_assoc k rev_before = function
   | (k',b)::after when k=k' -> rev_before,b,after
   | h::tail -> list_split_assoc k (h::rev_before) tail
 
-let rec list_fold_map2 f e = function
-  |  []  -> (e,[],[])
-  |  h::t ->
-       let e',h1',h2' = f e h in
-       let e'',t1',t2' = list_fold_map2 f e' t in
-	 e'',h1'::t1',h2'::t2'
-
 let discr_resolver env mtb =
      match mtb.typ_expr with
 	SEBstruct _ -> 
diff --git a/kernel/term.ml b/kernel/term.ml
index 492ebbb0d..88bc4cc4e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -285,14 +285,6 @@ let kind_of_term2 c = c
 
 let kind_of_term = kind_of_term
 
-
-(* En vue d'un kind_of_type : constr -> hnftype ??? *)
-type hnftype =
-  | HnfSort   of sorts
-  | HnfProd   of name * constr * constr
-  | HnfAtom   of constr
-  | HnfInd of inductive * constr array
-
 (**********************************************************************)
 (*          Non primitive term destructors                            *)
 (**********************************************************************)
@@ -346,18 +338,12 @@ let rec is_Type c = match kind_of_term c with
   | Cast (c,_,_) -> is_Type c
   | _ -> false
 
-let isType = function
-  | Type _ -> true
-  | _ -> false
-
 let is_small = function
   | Prop _ -> true
   | _ -> false
 
 let iskind c = isprop c or is_Type c
 
-let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2)
-
 (* Tests if an evar *)
 let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false
 
@@ -424,10 +410,6 @@ let destEvar c = match kind_of_term c with
   | Evar (kn, a as r) -> r
   | _ -> invalid_arg "destEvar"
 
-let num_of_evar c = match kind_of_term c with
-  | Evar (n, _) -> n
-  | _ -> anomaly "num_of_evar called with bad args"
-
 (* Destructs a (co)inductive type named kn *)
 let destInd c = match kind_of_term c with
   | Ind (kn, a as r) -> r
@@ -497,18 +479,6 @@ let decompose_app c =
     | App (f,cl) -> (f, Array.to_list cl)
     | _ -> (c,[])
 
-(* strips head casts and flattens head applications *)
-let rec strip_head_cast c = match kind_of_term c with
-  | App (f,cl) ->
-      let rec collapse_rec f cl2 = match kind_of_term f with
-	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-	| Cast (c,_,_) -> collapse_rec c cl2
-	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
-      in
-      collapse_rec f cl
-  | Cast (c,_,_) -> strip_head_cast c
-  | _ -> c
-
 (****************************************************************************)
 (*              Functions to recur through subterms                         *)
 (****************************************************************************)
@@ -899,12 +869,10 @@ let mkCast = mkCast
 (* Constructs the product (x:t1)t2 *)
 let mkProd = mkProd
 let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c)
-let mkProd_string   s t c = mkProd (Name (id_of_string s), t, c)
 
 (* Constructs the abstraction [x:t1]t2 *)
 let mkLambda = mkLambda
 let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c)
-let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 (* Constructs [x=c_1:t]c_2 *)
 let mkLetIn = mkLetIn
@@ -933,11 +901,6 @@ let mkNamedLambda_or_LetIn (id,body,t) c =
     | Some b -> mkNamedLetIn id b t c
 
 (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
-let mkProd_wo_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na,  t, c)
-    | Some b -> subst1 b c
-
 let mkNamedProd_wo_LetIn (id,body,t) c =
   match body with
     | None -> mkNamedProd id t c
@@ -951,11 +914,6 @@ let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
    function is not itself an applicative term *)
 let mkApp = mkApp
 
-let mkAppA v =
-  let l = Array.length v in
-  if l=0 then anomaly "mkAppA received an empty array"
-  else mkApp (v.(0), Array.sub v 1 (Array.length v -1))
-
 (* Constructs a constant *)
 (* The array of terms correspond to the variables introduced in the section *)
 let mkConst = mkConst
@@ -974,7 +932,6 @@ let mkConstruct = mkConstruct
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
 let mkCase = mkCase
-let mkCaseL (ci, p, c, ac) = mkCase (ci, p, c, Array.of_list ac)
 
 (* If recindxs = [|i1,...in|]
       funnames = [|f1,...fn|]
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 183a27935..3d2461237 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -18,7 +18,6 @@ open Reduction
 open Inductive
 open Type_errors
 
-let conv = default_conv CONV
 let conv_leq = default_conv CUMUL
 
 let conv_leq_vecti env v1 v2 =
@@ -45,8 +44,6 @@ let assumption_of_judgment env j =
   with TypeError _ ->
     error_assumption env j
 
-let sort_judgment env j = (type_judgment env j).utj_type
-
 (************************************************)
 (* Incremental typing rules: builds a typing judgement given the *)
 (* judgements for the subterms. *)
@@ -474,8 +471,6 @@ and execute_recdef env (names,lar,vdef) i cu =
 
 and execute_array env = array_fold_map' (execute env)
 
-and execute_list env = list_fold_map' (execute env)
-
 (* Derived functions *)
 let infer env constr =
   let (j,(cst,_)) =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9854cdc1d..40bd2a20d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -568,16 +568,6 @@ let no_upper_constraints u cst =
 
 (* Pretty-printing *)
 
-let num_universes g =
-  UniverseLMap.fold (fun _ _ -> succ) g 0
-
-let num_edges g =
-  let reln_len = function
-    | Equiv _ -> 1
-    | Canonical {lt=lt;le=le} -> List.length lt + List.length le
-  in
-  UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0
-
 let pr_arc = function
   | Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 90fb56d86..51528dbf2 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -538,12 +538,6 @@ let branch_of_switch k sw =
 
 (* Evaluation *)
 
-
-let is_accu v =
-  let o = Obj.repr v in
-  Obj.is_block o && Obj.tag o = accu_tag &&
-  fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag
-
 let rec whd_stack v stk =
   match stk with
   | [] -> whd_val v