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, 6 insertions, 137 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b8c13a2f7..cc9aa0060 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -749,16 +749,6 @@ let insert_aliases env sigma alias eqns =
 (**********************************************************************)
 (* Functions to deal with elimination predicate *)
 
-exception Occur
-let noccur_between_without_evar n m term =
-  let rec occur_rec n c = match kind_of_term c with
-    | Rel p       -> if n<=p && p<n+m then raise Occur
-    | Evar (_,cl) -> ()
-    | _             -> iter_constr_with_binders succ occur_rec n c
-  in
-  (m = 0) or (try occur_rec n term; true with Occur -> false)
-
-
 (* Infering the predicate *)
 (*
 The problem to solve is the following:
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 66263aee3..85112c288 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -92,13 +92,6 @@ let rec shift_value n = function
 let shift_value n v =
   if n = 0 then v else shift_value n v
 
-let rec shift_stack n = function
-    TOP -> TOP
-  | APP(v,stk) -> APP(Array.map (shift_value n) v, shift_stack n stk)
-  | CASE(c,b,i,s,stk) -> CASE(c,b,i,subs_shft(n,s), shift_stack n stk)
-let shift_stack n stk =
-  if n = 0 then stk else shift_stack n stk
-
 (* Contracts a fixpoint: given a fixpoint and a bindings,
  * returns the corresponding fixpoint body, and the bindings in which
  * it should be evaluated: its first variables are the fixpoint bodies
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 73ce8134f..2d2677ee0 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -398,7 +398,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
 let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
   if stre = Local then Dispose else Substitute obj
 
-let (inCoercion,_) =
+let inCoercion =
   declare_object {(default_object "COERCION") with
     open_function = open_coercion;
     load_function = load_coercion;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0dcaf1444..04dc13290 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -166,8 +166,6 @@ let computable p k =
   &&
   noccur_between 1 (k+1) ccl
 
-let avoid_flag isgoal = if isgoal then Some true else None
-
 let lookup_name_as_displayed env t s =
   let rec lookup avoid n c = match kind_of_term c with
     | Prod (name,_,c') ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3f899a8ec..4ad823e06 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1394,33 +1394,8 @@ let check_evars env initial_sigma sigma c =
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
-(* Substitutes undefined evars by evars of same context up to renaming *)
-
-let subst_evar_evar subst c =
-  let rec aux c = match kind_of_term c with
-  | Evar (evk,args) ->
-      let evk' = try ExistentialMap.find evk subst with Not_found -> evk in
-      mkEvar (evk',Array.map aux args)
-  | _ -> map_constr aux c
-  in aux c
-
-let subst_undefined_evar_info_evar subst evi =
-  { evi with
-    evar_hyps = map_named_val (subst_evar_evar subst) evi.evar_hyps;
-    evar_concl = subst_evar_evar subst evi.evar_concl }
-
 open Rawterm
 
-let subst_evar_evar_in_constr_with_bindings subst (c,bl) =
-  (subst_evar_evar subst c,
-   match bl with
-   | ImplicitBindings largs ->
-       ImplicitBindings (List.map (subst_evar_evar subst) largs)
-   | ExplicitBindings lbind ->
-       ExplicitBindings (List.map (on_pi3 (subst_evar_evar subst)) lbind)
-   | NoBindings ->
-       NoBindings)
-
 (* Operations on value/type constraints *)
 
 type type_constraint_type = (int * int) option * constr
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 22f0c256d..c70c13d9e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -96,8 +96,6 @@ module EvarInfoMap = struct
   type t = evar_info ExistentialMap.t * evar_info ExistentialMap.t
 
   let empty = ExistentialMap.empty, ExistentialMap.empty
-  let is_empty (def,undef) =
-    (ExistentialMap.is_empty def, ExistentialMap.is_empty undef)
 
   let to_list (def,undef) =
     (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 8a0966ae3..5bd8b44f9 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -146,9 +146,6 @@ let make_case_info env ind style =
     ci_cstr_ndecls = mip.mind_consnrealdecls;
     ci_pp_info = print_info }
 
-let make_default_case_info env style ind =
-  make_case_info env ind style
-
 (*s Useful functions *)
 
 type constructor_summary = {
@@ -200,12 +197,6 @@ let get_constructors env (ind,params) =
   Array.init (Array.length mip.mind_consnames)
     (fun j -> get_constructor (ind,mib,mip,params) (j+1))
 
-let rec instantiate args c = match kind_of_term c, args with
-  | Prod (_,_,c), a::args -> instantiate args (subst1 a c)
-  | LetIn (_,b,_,c), args -> instantiate args (subst1 b c)
-  | _, [] -> c
-  | _ -> anomaly "too short arity"
-
 (* substitution in a signature *)
 
 let substnl_rel_context subst n sign =
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 3f117786c..b971db135 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -85,13 +85,6 @@ let build_lambda toabstract stk (m : constr) =
   in
   buildrec m 1 stk
 
-let memb_metavars m n =
-  match (m,n) with
-    | (None, _)     -> true
-    | (Some mvs, n) -> List.mem n mvs
-
-let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
-
 let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
   match ind with
   | Some ind -> ind = ci2.ci_ind
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index c703d5be7..15bc06e02 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -59,12 +59,6 @@ let rec occur_meta_pattern = function
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
-type constr_label =
-  | ConstNode of constant
-  | IndNode of inductive
-  | CstrNode of constructor
-  | VarNode of identifier
-
 exception BoundPattern;;
 
 let rec head_pattern_bound t =
@@ -155,8 +149,6 @@ let map_pattern_with_binders g f l = function
   (* Bound to terms *)
   | PFix _ | PCoFix _ as x) -> x
 
-let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) ()
-
 let error_instantiate_pattern id l =
   let is = if List.length l = 1 then "is" else "are" in
   errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f75f4990a..d477ec34a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -76,7 +76,7 @@ let discharge_structure (_,(ind,id,kl,projs)) =
   Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
         List.map (Option.map Lib.discharge_con) projs)
 
-let (inStruc,outStruc) =
+let inStruc =
   declare_object {(default_object "STRUCTURE") with
     cache_function = cache_structure;
     load_function = load_structure;
@@ -135,7 +135,7 @@ open Libobject
 let load_method (_,(ty,id)) =
   meth_dnet := MethodsDnet.add ty id !meth_dnet
 
-let (in_method,out_method) =
+let in_method =
   declare_object
     { (default_object "RECMETHODS") with
 	load_function = (fun _ -> load_method);
@@ -290,7 +290,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
 let discharge_canonical_structure (_,(cst,ind)) =
   Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
 
-let (inCanonStruc,outCanonStruct) =
+let inCanonStruc =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
     open_function = open_canonical_structure;
     cache_function = cache_canonical_structure;
@@ -328,8 +328,6 @@ let check_and_decompose_canonical_structure ref =
 let declare_canonical_structure ref =
   add_canonical_structure (check_and_decompose_canonical_structure ref)
 
-let outCanonicalStructure x = fst (outCanonStruct x)
-
 let lookup_canonical_conversion (proj,pat) =
   List.assoc pat (Refmap.find proj !object_table)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 78a5341b1..689e544b8 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -42,13 +42,6 @@ let append_stack_list l s =
   | (l1, s) -> Zapp l1 :: s
 let append_stack v s = append_stack_list (Array.to_list v) s
 
-(* Collapse the shifts in the stack *)
-let zshift n s =
-  match (n,s) with
-      (0,_) -> s
-    | (_,Zshift(k)::s) -> Zshift(n+k)::s
-    | _ -> Zshift(n)::s
-
 let rec stack_args_size = function
   | Zapp l::s -> List.length l + stack_args_size s
   | Zshift(_)::s -> stack_args_size s
@@ -61,10 +54,6 @@ let rec decomp_stack = function
   | Zapp(v::l)::s -> Some (v, (Zapp l :: s))
   | Zapp [] :: s -> decomp_stack s
   | _ -> None
-let rec decomp_stackn = function
-  | Zapp [] :: s -> decomp_stackn s
-  | Zapp l :: s -> (Array.of_list l, s)
-  | _ -> assert false
 let array_of_stack s =
   let rec stackrec = function
   | [] -> []
@@ -153,10 +142,6 @@ let whd_stack sigma x =
   appterm_of_stack (whd_app_state sigma (x, empty_stack))
 let whd_castapp_stack = whd_stack
 
-let stack_reduction_of_reduction red_fun env sigma s =
-  let t = red_fun env sigma (app_stack s) in
-  whd_stack t
-
 let strong whdfun env sigma t =
   let rec strongrec env t =
     map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
@@ -584,14 +569,6 @@ let rec whd_betaiota_preserving_vm_cast env sigma t =
 let nf_betaiota_preserving_vm_cast =
   strong whd_betaiota_preserving_vm_cast
 
-(* lazy weak head reduction functions *)
-let whd_flags flgs env sigma t =
-  try
-    whd_val
-      (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
-      (inject t)
-  with Anomaly _ -> error "Tried to normalized ill-typed term" 
-
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
@@ -924,17 +901,6 @@ let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
 
 (* Instantiate metas that create beta/iota redexes *)
 
-let meta_value evd mv =
-  let rec valrec mv =
-    match meta_opt_fvalue evd mv with
-    | Some (b,_) ->
-      instance evd
-        (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
-        b.rebus
-    | None -> mkMeta mv
-  in
-  valrec mv
-
 let meta_reducible_instance evd b =
   let fm = Metaset.elements b.freemetas in
   let metas = List.fold_left (fun l mv ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a7a5d84c1..e99baa291 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -299,17 +299,6 @@ let reference_eval sigma env = function
        end)
   | ref -> compute_consteval sigma env ref
 
-let rev_firstn_liftn fn ln =
-  let rec rfprec p res l =
-    if p = 0 then
-      res
-    else
-      match l with
-        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
-        | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
-  in
-  rfprec fn []
-
 (* If f is bound to EliminationFix (n',infos), then n' is the minimal
    number of args for starting the reduction and infos is
    (nbfix,[(yi1,Ti1);...;(yip,Tip)],n) indicating that f converts
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 93418c6e6..17e052223 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -32,7 +32,6 @@ let pr_name = function
   | Name id -> pr_id id
   | Anonymous -> str "_"
 
-let pr_path sp = str(string_of_kn sp)
 let pr_con sp = str(string_of_con sp)
 
 let rec pr_constr c = match kind_of_term c with
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b381f295c..b1cbed4af 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -32,10 +32,6 @@ let register_set_typeclass_transparency =
   (:=) set_typeclass_transparency_ref
 let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c
 
-let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
-(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
-let mismatched_props env n m = mismatched_ctx_inst env Properties n m
-
 type rels = constr list
 
 (* This module defines type-classes *)
@@ -197,7 +193,7 @@ let discharge_class (_,cl) =
 
 let rebuild_class cl = cl
 
-let (class_input,class_output) =
+let class_input =
   declare_object
     { (default_object "type classes state") with
       cache_function = cache_class;
@@ -246,7 +242,7 @@ let classify_instance inst =
   if inst.is_global = -1 then Dispose
   else Substitute inst
 
-let (instance_input,instance_output) =
+let instance_input =
   declare_object
     { (default_object "type classes instances state") with
       cache_function = cache_instance;
@@ -304,13 +300,6 @@ let instance_constructor cl args =
 
 let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
 
-let cmapl_add x y m =
-  try
-    let l = Gmap.find x m in
-    Gmap.add x (Gmap.add y.is_impl y l) m
-  with Not_found ->
-    Gmap.add x (Gmap.add y.is_impl y Gmap.empty) m
-
 let cmap_elements c = Gmap.fold (fun k v acc -> v :: acc) c []
 
 let instances_of c =
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8340af0fc..c39be8b68 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -190,8 +190,6 @@ and execute_recdef env evdref (names,lar,vdef) =
 
 and execute_array env evdref = Array.map (execute env evdref)
 
-and execute_list env evdref = List.map (execute env evdref)
-
 let check env evd c t =
   let evdref = ref evd in
   let j = execute env evdref c in