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

12 files changed, 8 insertions, 66 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c06fbfc685..821fc0fadf 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -65,13 +65,6 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
 type binder_list = (identifier located * bool * constr_expr) list
 
-(* Calls to interpretation functions. *)
-
-let interp_type_evars evdref env ?(impls=empty_internalization_env) typ =
-  let typ' = intern_gen true ~impls !evdref env typ in
-  let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
-    imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
-
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
 open Topconstr
@@ -281,14 +274,6 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
-let push_named_context = List.fold_right push_named
-
-let rec list_filter_map f = function
-  | [] -> []
-  | hd :: tl -> match f hd with
-    | None -> list_filter_map f tl
-    | Some x -> x :: list_filter_map f tl
-
 let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let evars = ref Evd.empty in
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index c4b7759123..8df17350c7 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -173,9 +173,6 @@ let rec attribute_of_vernac_command = function
   | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
   | VernacExtend _ -> []
   
-let is_vernac_goal_starting_command com =
-  List.mem GoalStartingCommand (attribute_of_vernac_command com)
-
 let is_vernac_navigation_command com =
   List.mem NavigationCommand (attribute_of_vernac_command com)
 
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 3440f9fe85..daa93a7e66 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -51,7 +51,7 @@ let discharge_scheme (_,(kind,l)) =
   Some (kind,Array.map (fun (ind,const) ->
     (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
 
-let (inScheme,_) =
+let inScheme =
   declare_object {(default_object "SCHEME") with
                     cache_function = cache_scheme;
                     load_function = (fun _ -> cache_scheme);
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 41680036c3..c182fb3854 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.ml
@@ -71,7 +71,7 @@ let subst a b = Profile.profile2 subst_key TypeDnet.subst a b
 let load_key = Profile.declare_profile "load"
 let load a = Profile.profile1 load_key load a
 *)
-let (input,output) =
+let input =
   declare_object
     { (default_object "LIBTYPES") with
 	load_function = (fun _ -> load);
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index efaf7707c3..f0cfd5fd97 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -32,7 +32,7 @@ open Nameops
 
 let cache_token (_,s) = add_keyword s
 
-let (inToken, outToken) =
+let inToken =
   declare_object {(default_object "TOKEN") with
        open_function = (fun i o -> if i=1 then cache_token o);
        cache_function = cache_token;
@@ -70,7 +70,7 @@ let subst_tactic_parule subst (key,n,p,(d,tac)) =
 let subst_tactic_notation (subst,(pa,pp)) =
   (subst_tactic_parule subst pa,pp)
 
-let (inTacticGrammar, outTacticGrammar) =
+let inTacticGrammar =
   declare_object {(default_object "TacticGrammar") with
        open_function = (fun i o -> if i=1 then cache_tactic_notation o);
        cache_function = cache_tactic_notation;
@@ -363,11 +363,6 @@ let error_not_same_scope x y =
   error ("Variables "^string_of_id x^" and "^string_of_id y^
     " must be in the same scope.")
 
-let error_both_bound_and_binding x y =
-  errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++
-  strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder \
-  for both terms and binders.")
-
 (**********************************************************************)
 (* Build pretty-printing rules                                        *)
 
@@ -403,12 +398,6 @@ let is_right_bracket s =
   let l = String.length s in l <> 0 &
   (s.[l-1] = '}' or s.[l-1] = ']' or s.[l-1] = ')')
 
-let is_left_bracket_on_left s =
-  let l = String.length s in l <> 0 & s.[l-1] = '>'
-
-let is_right_bracket_on_right s =
-  let l = String.length s in l <> 0 & s.[0] = '<'
-
 let is_comma s =
   let l = String.length s in l <> 0 &
   (s.[0] = ',' or s.[0] = ';')
@@ -726,7 +715,7 @@ let subst_syntax_extension (subst,(local,sy)) =
 let classify_syntax_definition (local,_ as o) =
   if local then Dispose else Substitute o
 
-let (inSyntaxExtension, outSyntaxExtension) =
+let inSyntaxExtension =
   declare_object {(default_object "SYNTAX-EXTENSION") with
        open_function = (fun i o -> if i=1 then cache_syntax_extension o);
        cache_function = cache_syntax_extension;
@@ -976,7 +965,7 @@ let subst_notation (subst,(lc,scope,pat,b,ndf)) =
 let classify_notation (local,_,_,_,_ as o) =
   if local then Dispose else Substitute o
 
-let (inNotation, outNotation) =
+let inNotation =
   declare_object {(default_object "NOTATION") with
        open_function = open_notation;
        cache_function = cache_notation;
@@ -1152,7 +1141,7 @@ let subst_scope_command (subst,(scope,o as x)) = match o with
       scope, ScopeClasses cl'
   | _ -> x
 
-let (inScopeCommand,outScopeCommand) =
+let inScopeCommand =
   declare_object {(default_object "DELIMITERS") with
       cache_function = cache_scope_command;
       open_function = open_scope_command;
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index ccb6c47749..429d39e205 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -217,8 +217,6 @@ let file_of_name name =
     coqtop could always load plugins, we prefer to have uniformity between
     bytecode and native versions. *)
 
-let stdlib_use_plugins = Coq_config.has_natdynlink
-
 (* [known_loaded_module] contains the names of the loaded ML modules
  * (linked or loaded with load_object). It is used not to load a
  * module twice. It is NOT the list of ML modules Coq knows. *)
@@ -298,7 +296,7 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 let classify_ml_module_object ({mlocal=mlocal} as o) =
   if mlocal then Dispose else Substitute o
 
-let (inMLModule,outMLModule) =
+let inMLModule =
   declare_object {(default_object "ML-MODULE") with
                     load_function = (fun _ -> cache_ml_module_object);
                     cache_function = cache_ml_module_object;
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index f624d40a73..c625854eae 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -61,8 +61,6 @@ type ml_module_object = {
   mlocal: Vernacexpr.locality_flag;
   mnames: string list;
 }
-val inMLModule : ml_module_object -> Libobject.obj
-val outMLModule : Libobject.obj -> ml_module_object
 
 val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0dd18f0641..1ef51496b1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -277,9 +277,6 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
-let qualid_of_con c = 
-  Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
-
 let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
   let _, r = decompose_prod_assum instance in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index abb0af108b..e01978dc14 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -93,10 +93,6 @@ let rec head c =
   | LetIn (_,_,_,c) -> head c
   | _              -> c
 
-let constr_to_full_path c = match kind_of_term c with
-  | Const sp -> sp
-  | _ -> raise No_full_path
-
 let xor a b = (a or b) & (not (a & b))
 
 let plain_display ref a c =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index eae6751776..b7524eea0d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -20,7 +20,6 @@ open Tacmach
 open Constrintern
 open Prettyp
 open Printer
-open Tactic_printer
 open Tacinterp
 open Command
 open Goptions
@@ -1161,16 +1160,6 @@ let vernac_locate = function
 (********************)
 (* Proof management *)
 
-let vernac_goal = function
-  | None -> ()
-  | Some c ->
-      if not (refining()) then begin
-        let unnamed_kind = Lemma (* Arbitrary *) in
-        start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->());
-	print_subgoals ()
-      end else
-	error "repeated Goal not permitted in refining mode."
-
 let vernac_abort = function
   | None ->
       delete_current_proof ();
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index cdf72bb1e1..224d9765f3 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -372,9 +372,6 @@ let locality_flag = ref None
 
 let local_of_bool = function true -> Local | false -> Global
 
-let is_true = function Some (_,b) -> b | _ -> false
-let is_false = function Some (_,b) -> not b | _ -> false
-
 let check_locality () =
   match !locality_flag with
   | Some (loc,true) -> 
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 878b0fdf8d..10c5a00f68 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -64,7 +64,3 @@ let call (opn,converted_args) =
         if !Flags.debug then
 	  msgnl (str"Vernac Interpreter " ++ str !loc);
         raise e
-
-let bad_vernac_args s =
-  anomalylabstrm s
-    (str"Vernac " ++ str s ++ str" called with bad arguments")