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

5 files changed, 4 insertions, 41 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index d2d399f100..11c5bf398d 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -29,10 +29,6 @@ open Safe_typing
 
 let strength_min l = if List.mem Local l then Local else Global
 
-let id_of_varid c = match kind_of_term c with
-  | Var id -> id
-  | _ -> anomaly "class__id_of_varid"
-
 (* Errors *)
 
 type coercion_error_kind =
@@ -103,15 +99,6 @@ let uniform_cond nargs lt =
   in 
   aux (nargs,lt)
 
-let id_of_cl  = function
-  | CL_FUN -> id_of_string "FUNCLASS"
-  | CL_SORT -> id_of_string "SORTCLASS"
-  | CL_CONST kn -> id_of_label (con_label kn)
-  | CL_IND ind ->
-      let (_,mip) = Global.lookup_inductive ind in
-      mip.mind_typename
-  | CL_SECVAR id -> id
-
 let class_of_global = function
   | ConstRef sp -> CL_CONST sp
   | IndRef sp -> CL_IND sp
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b6c6640207..e5c3322a35 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -37,10 +37,6 @@ let typeclasses_db = "typeclass_instances"
 let qualid_of_con c = 
   Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
 
-let set_rigid c = 
-  Auto.add_hints false [typeclasses_db] 
-    (Vernacexpr.HintsTransparency ([qualid_of_con c], false))
-
 let _ =
   Typeclasses.register_add_instance_hint 
     (fun inst pri ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6e000bc74a..d07c4973e0 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -47,9 +47,6 @@ open Mod_subst
 open Evd
 open Decls
 
-let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b))
-let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b))
-
 let rec abstract_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
@@ -73,14 +70,6 @@ let rec under_binders env f n c =
 	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
       | _ -> assert false
 
-let rec destSubCast c = match kind_of_term c with
-  | Lambda (x,t,c) -> 
-      let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
-  | LetIn (x,b,t,c) ->
-      let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u)
-  | Cast (b,_, u) -> (b,u)
-  | _ -> assert false
-
 let rec complete_conclusion a cs = function
   | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
   | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
@@ -288,7 +277,7 @@ let _ =
       optwrite = (fun b -> eq_flag := b) }
 
 (* boolean equality *)
-let (inScheme,outScheme) =  
+let (inScheme,_) =  
   declare_object {(default_object "EQSCHEME") with 
                     cache_function = Ind_tables.cache_scheme; 
                     load_function = (fun _ -> Ind_tables.cache_scheme); 
@@ -321,21 +310,21 @@ let declare_eq_scheme sp =
 (* decidability of eq *)
 
 
-let (inBoolLeib,outBoolLeib) =
+let (inBoolLeib,_) =
   declare_object {(default_object "BOOLLIEB") with
                     cache_function = Ind_tables.cache_bl;
                     load_function = (fun _ -> Ind_tables.cache_bl);
                     subst_function = Auto_ind_decl.subst_in_constr;
                     export_function = Ind_tables.export_bool_leib }
 
-let (inLeibBool,outLeibBool) =
+let (inLeibBool,_) =
   declare_object {(default_object "LIEBBOOL") with
                     cache_function = Ind_tables.cache_lb;
                     load_function = (fun _ -> Ind_tables.cache_lb);
                     subst_function = Auto_ind_decl.subst_in_constr;
                     export_function = Ind_tables.export_leib_bool }
 
-let (inDec,outDec) =
+let (inDec,_) =
   declare_object {(default_object "EQDEC") with
                     cache_function = Ind_tables.cache_dec;
                     load_function = (fun _ -> Ind_tables.cache_dec);
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e736fc676e..729db2d02a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -51,9 +51,6 @@ let load_rcfile() =
   else 
     Flags.if_verbose msgnl (str"Skipping rcfile loading.")
 
-let add_ml_include s =
-  Mltop.add_ml_dir s
-
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path d s =
   Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
@@ -64,11 +61,6 @@ let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
 let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
-(* Because find puts "./" and the loadpath is not nicely pretty-printed *)
-let hm2 s = 
-  let n = String.length s in
-  if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s
-
 (* The list of all theories in the standard library /!\ order does matter *)
 let theories_dirs_map = [
     "theories/Unicode", "Unicode" ;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cd13c6c880..da63382bf4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -72,7 +72,6 @@ let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
 let set_default_include d = push_include (d,Nameops.default_root_prefix)
-let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix)
 let set_include d p =
   let p = dirpath_of_string p in
   Library.check_coq_overwriting p;