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

7 files changed, 12 insertions, 28 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 2a4b2e403..9e242d2b3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -75,7 +75,7 @@ let discharge_variable (_,o) = match o with
   | Inr (id,_) -> Some (Inl (variable_constraints id))
   | Inl _ -> Some o
 
-let (inVariable, outVariable) =
+let (inVariable,_) =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     discharge_function = discharge_variable;
@@ -143,7 +143,7 @@ let export_constant cst = Some (dummy_constant cst)
 
 let classify_constant (_,cst) = Substitute (dummy_constant cst)
 
-let (inConstant, outConstant) =
+let (inConstant,_) =
   declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -262,7 +262,7 @@ let dummy_inductive_entry (_,m) = ([],{
 
 let export_inductive x = Some (dummy_inductive_entry x)
 
-let (inInductive, outInductive) =
+let (inInductive,_) =
   declare_object {(default_object "INDUCTIVE") with 
     cache_function = cache_inductive;
     load_function = load_inductive;
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 129ea4ef2..52fa94569 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -114,11 +114,6 @@ let mp_of_kn kn =
     else
       anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
 
-let is_bound mp =
-  match mp with
-    | MPbound _ -> true
-    | _ -> false
-
 let dir_of_sp sp = 
   let dir,id = repr_path sp in
     extend_dirpath dir id
@@ -490,7 +485,7 @@ let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
     open_objects i (dirpath,(mp,empty_dirpath)) seg
 
-let (in_modkeep,out_modkeep) = 
+let (in_modkeep,_) =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
@@ -575,7 +570,7 @@ let classify_modtype (_,(_,substobjs)) =
   Substitute (None,substobjs)
 
 
-let (in_modtype,out_modtype) =
+let (in_modtype,_) =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
       open_function = open_modtype;
@@ -859,7 +854,7 @@ let subst_import (_,subst,(export,mp as obj)) =
     if mp'==mp then obj else
       (export,mp')
 	
-let (in_import,out_import) = 
+let (in_import,_) =
   declare_object {(default_object "IMPORT MODULE") with
 		    cache_function = cache_import;
 		    open_function = (fun i o -> if i=1 then cache_import o);
diff --git a/library/decls.ml b/library/decls.ml
index 8a67de4ec..5a8729215 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -70,7 +70,3 @@ let last_section_hyps dir =
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
     ~init:[]
-
-let is_section_variable = function
-  | VarRef _ -> true
-  | _ -> false
diff --git a/library/goptions.ml b/library/goptions.ml
index b614ed34a..b5a8b00ea 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -77,8 +77,7 @@ module MakeTable =
       if List.mem_assoc nick !A.table then
 	error "Sorry, this table name is already used"
 
-    module MyType = struct type t = A.t let compare = Pervasives.compare end
-    module MySet = Set.Make(MyType)
+    module MySet = Set.Make (struct type t = A.t let compare = compare end)
 
     let t = ref (MySet.empty : MySet.t)
 
@@ -219,8 +218,8 @@ type 'a option_sig = {
 
 type option_type = bool * (unit -> value) -> (value -> unit) 
 
-module Key = struct type t = option_name let compare = Pervasives.compare end
-module OptionMap = Map.Make(Key)
+module OptionMap =
+  Map.Make (struct  type t = option_name let compare = compare end)
 
 let value_tab = ref OptionMap.empty
 
diff --git a/library/heads.ml b/library/heads.ml
index 1b1dba43f..ea3acbbe8 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -39,12 +39,8 @@ type head_approximation =
 
 (** Registration as global tables and rollback. *)
 
-module Evalreford = struct
-  type t = evaluable_global_reference
-  let compare = Pervasives.compare
-end
-
-module Evalrefmap = Map.Make(Evalreford)
+module Evalrefmap =
+  Map.Make (struct type t = evaluable_global_reference let compare = compare end)
 
 let head_map = ref Evalrefmap.empty
 
diff --git a/library/libnames.ml b/library/libnames.ml
index f0fcd94c9..44da7b6de 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -66,8 +66,6 @@ module RefOrdered =
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
 
-let inductives_table = ref Indmap.empty
-
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
diff --git a/library/libobject.mli b/library/libobject.mli
index 61e650e6b..d104635cd 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -102,7 +102,7 @@ val ident_subst_function : object_name * substitution * 'a -> 'a
 
 type obj
 
-val declare_object : 
+val declare_object :
   'a object_declaration -> ('a -> obj) * (obj -> 'a)
 
 val object_tag : obj -> string