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

11 files changed, 0 insertions, 237 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8931d67f3..12cffc492 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -107,18 +107,6 @@ let ident_colon =
               | _ -> err ())
         | _ -> err ())
 
-let ident_with =
-  Gram.Entry.of_parser "ident_with"
-    (fun strm ->
-      match get_tok (stream_nth 0 strm) with
-      | IDENT s ->
-          (match get_tok (stream_nth 1 strm) with
-             | KEYWORD "with" ->
-		 stream_njunk 2 strm;
-		 Names.id_of_string s
-             | _ -> err ())
-      | _ -> err ())
-
 let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
 
 GEXTEND Gram
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f9e146730..9b476d996 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -93,24 +93,6 @@ let check_for_coloneq =
       | KEYWORD "(" -> skip_binders 2
       | _ -> err ())
 
-let guess_lpar_ipat s strm =
-  match get_tok (stream_nth 0 strm) with
-    | KEYWORD "(" ->
-        (match get_tok (stream_nth 1 strm) with
-          | KEYWORD ("("|"[") -> ()
-          | IDENT _ ->
-              (match get_tok (stream_nth 2 strm) with
-                | KEYWORD s' when s = s' -> ()
-                | _ -> err ())
-          | _ -> err ())
-    | _ -> err ()
-
-let guess_lpar_coloneq =
-  Gram.Entry.of_parser "guess_lpar_coloneq" (guess_lpar_ipat ":=")
-
-let guess_lpar_colon =
-  Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":")
-
 let lookup_at_as_coma =
   Gram.Entry.of_parser "lookup_at_as_coma"
     (fun strm ->
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index d1168ad19..15cdc6077 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -250,8 +250,6 @@ let rec number len = parser
   | [< ' ('0'..'9' as c); s >] -> number (store len c) s
   | [< >] -> len
 
-let escape len c = store len c
-
 let rec string in_comments bp len = parser
   | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
       if esc then string in_comments bp (store len '"') s else len
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 95948d2ac..034c46e58 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -264,13 +264,6 @@ let get_univ s =
 
 let get_entry (u, utab) s = Hashtbl.find utab s
 
-let get_entry_type (u, utab) s =
-  try
-    type_of_typed_entry (get_entry (u, utab) s)
-  with Not_found ->
-    errorlabstrm "Pcoq.get_entry"
-      (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".")
-
 let new_entry etyp (u, utab) s =
   if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr);
   let ename = u ^ ":" ^ s in
@@ -340,7 +333,6 @@ module Prim =
 module Constr =
   struct
     let gec_constr = make_gen_entry uconstr rawwit_constr
-    let gec_constr_list = make_gen_entry uconstr (wit_list0 rawwit_constr)
 
     (* Entries that can be refered via the string -> Gram.entry table *)
     let constr = gec_constr "constr"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c7edd9b92..7db89a5ff 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -147,11 +147,6 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
-(*
-val get_entry : gram_universe -> string -> typed_entry
-val get_entry_type : gram_universe -> string -> entry_type
-*)
-
 val create_entry : gram_universe -> string -> entry_type -> typed_entry
 val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
   'a Gram.entry
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 6276a23c3..9bfa32285 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -22,14 +22,10 @@ open Constrextern
 open Termops
 (*i*)
 
-let sep_p = fun _ -> str"."
 let sep_v = fun _ -> str"," ++ spc()
-let sep_pp = fun _ -> str":"
-let sep_bar = fun _ -> spc() ++ str"| "
 let pr_tight_coma () = str "," ++ cut ()
 
 let latom = 0
-let lannot = 100
 let lprod = 200
 let llambda = 200
 let lif = 200
@@ -108,10 +104,6 @@ let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
 
 let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
-let pr_optc pr = function
-  | None -> mt ()
-  | Some x -> pr_sep_com spc pr x
-
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 
 let pr_universe = Univ.pr_uni
@@ -355,21 +347,6 @@ let pr_recursive pr_decl id = function
         (pr_decl true) dl ++
       fnl() ++ str "for " ++ pr_id id
 
-let is_var id = function
-  | CRef (Ident (_,id')) when id=id' -> true
-  | _ -> false
-
-let tm_clash = function
-  | (CRef (Ident (_,id)), Some (CApp (_,_,nal)))
-      when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false)
-	nal
-      -> Some id
-  | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal)))
-      when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false)
-	nal
-      -> Some id
-  | _ -> None
-
 let pr_asin pr (na,indnalopt) =
   (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
     | Some na -> spc () ++ str "as " ++  pr_lname na
@@ -387,8 +364,6 @@ let pr_case_type pr po =
     | Some p ->
         spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p)
 
-let pr_return_type pr po = pr_case_type pr po
-
 let pr_simple_return_type pr na po =
   (match na with
     | Some (_,Name id) ->
@@ -561,38 +536,6 @@ let pr pr sep inherited a =
   pr_with_comments loc
     (sep() ++ if prec_less prec inherited then strm else surround strm)
 
-
-let rec strip_context n iscast t =
-  if n = 0 then
-    [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
-  else match t with
-    | CLambdaN (loc,(nal,bk,t)::bll,c) ->
-	let n' = List.length nal in
-	if n' > n then
-	  let nal1,nal2 = list_chop n nal in
-	  [LocalRawAssum (nal1,bk,t)], CLambdaN (loc,(nal2,bk,t)::bll,c)
-	else
-	let bl', c = strip_context (n-n') iscast
-	  (if bll=[] then c else CLambdaN (loc,bll,c)) in
-	LocalRawAssum (nal,bk,t) :: bl', c
-    | CProdN (loc,(nal,bk,t)::bll,c) ->
-	let n' = List.length nal in
-	if n' > n then
-	  let nal1,nal2 = list_chop n nal in
-	  [LocalRawAssum (nal1,bk,t)], CProdN (loc,(nal2,bk,t)::bll,c)
-	else
-	let bl', c = strip_context (n-n') iscast
-	  (if bll=[] then c else CProdN (loc,bll,c)) in
-	LocalRawAssum (nal,bk,t) :: bl', c
-    | CArrow (loc,t,c) ->
-	let bl', c = strip_context (n-1) iscast c in
-	LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c
-    | CCast (_,c,_) -> strip_context n false c
-    | CLetIn (_,na,b,c) ->
-	let bl', c = strip_context (n-1) iscast c in
-	LocalRawDef (na,b) :: bl', c
-    | _ -> anomaly "strip_context"
-
 type term_pr = {
   pr_constr_expr   : constr_expr -> std_ppcmds;
   pr_lconstr_expr  : constr_expr -> std_ppcmds;
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 864b5b227..64b8b7bc9 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -90,8 +90,6 @@ let pr_quantified_hypothesis = function
   | AnonHyp n -> int n
   | NamedHyp id -> pr_id id
 
-let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
-
 let pr_binding prc = function
   | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
   | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
@@ -130,11 +128,6 @@ let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
 
 let with_evars ev s = if ev then "e" ^ s else s
 
-let out_bindings = function
-  | ImplicitBindings l -> ImplicitBindings (List.map snd l)
-  | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l)
-  | NoBindings -> NoBindings
-
 let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
 
 let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
@@ -294,8 +287,6 @@ let pr_extend prc prlc prtac prpat =
 (**********************************************************************)
 (* The tactic printer                                                 *)
 
-let sep_v = fun _ -> str"," ++ spc()
-
 let strip_prod_binders_expr n ty =
   let rec strip_ty acc n ty =
     match ty with
@@ -316,8 +307,6 @@ let pr_ltac_or_var pr = function
   | ArgArg x -> pr x
   | ArgVar (loc,id) -> pr_with_comments loc (pr_id id)
 
-let pr_arg pr x = spc () ++ pr x
-
 let pr_ltac_constant sp =
   pr_qualid (Nametab.shortest_qualid_of_tactic sp)
 
@@ -326,12 +315,6 @@ let pr_evaluable_reference_env env = function
   | EvalConstRef sp ->
       Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp)
 
-let pr_quantified_hypothesis = function
-  | AnonHyp n -> int n
-  | NamedHyp id -> pr_id id
-
-let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
-
 let pr_esubst prc l =
   let pr_qhyp = function
       (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
@@ -356,10 +339,6 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
 let pr_with_bindings prlc prc (c,bl) =
   hov 1 (prc c ++ pr_bindings prlc prc bl)
 
-let pr_with_constr prc = function
-  | None -> mt ()
-  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
-
 let pr_with_induction_names = function
   | None, None -> mt ()
   | eqpat, ipat ->
@@ -441,15 +420,6 @@ let pr_clauses default_is_concl pr_id = function
 	 (if occs = no_occurrences_expr then mt ()
 	  else pr_with_occurrences (fun () -> str" |- *") (occs,())))
 
-let pr_clause_pattern pr_id = function
-  | (None, []) -> mt ()
-  | (glopt,l) ->
-      str " in" ++
-      prlist
-        (fun (id,nl) -> prlist (pr_arg int) nl
-	  ++ spc () ++ pr_id id) l ++
-        pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt
-
 let pr_orient b = if b then mt () else str " <-"
 
 let pr_multi = function
@@ -546,20 +516,6 @@ let pr_auto_using prc = function
   | l -> spc () ++
       hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
-let pr_autoarg_adding = function
-  | [] -> mt ()
-  | l ->
-      spc () ++ str "adding [" ++
-        hv 0 (prlist_with_sep spc pr_reference l) ++ str "]"
-
-let pr_autoarg_destructing = function
-  | true -> spc () ++ str "destructing"
-  | false -> mt ()
-
-let pr_autoarg_usingTDB = function
-  | true -> spc () ++ str "using tdb"
-  | false -> mt ()
-
 let pr_then () = str ";"
 
 let ltop = (5,E)
@@ -1037,9 +993,6 @@ let rec raw_printers =
 and pr_raw_tactic_level env n (t:raw_tactic_expr) =
   fst (make_pr_tac raw_printers env) n t
 
-and pr_raw_match_rule env t =
-  snd (make_pr_tac raw_printers env) t
-
 let pr_and_constr_expr pr (c,_) = pr c
 
 let pr_pat_and_constr_expr b (c,_) =
@@ -1061,9 +1014,6 @@ let rec glob_printers =
 and pr_glob_tactic_level env n (t:glob_tactic_expr) =
   fst (make_pr_tac glob_printers env) n t
 
-and pr_glob_match_rule env t =
-  snd (make_pr_tac glob_printers env) t
-
 let pr_constr_or_lconstr_pattern b =
   if b then pr_lconstr_pattern else pr_constr_pattern
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b0ae6d139..ba3371ee3 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -84,27 +84,12 @@ let rec match_vernac_rule tys = function
       else match_vernac_rule tys rls
 
 let sep = fun _ -> spc()
-let sep_p = fun _ -> str"."
-let sep_v = fun _ -> str","
 let sep_v2 = fun _ -> str"," ++ spc()
-let sep_pp = fun _ -> str":"
 
 let pr_ne_sep sep pr = function
     [] -> mt()
   | l -> sep() ++ pr l
 
-let pr_entry_prec = function
-  | Some LeftA -> str"LEFTA "
-  | Some RightA -> str"RIGHTA "
-  | Some NonA -> str"NONA "
-  | None -> mt()
-
-let pr_prec = function
-  | Some LeftA -> str", left associativity"
-  | Some RightA -> str", right associativity"
-  | Some NonA -> str", no associativity"
-  | None -> mt()
-
 let pr_set_entry_type = function
   | ETName -> str"ident"
   | ETReference -> str"global"
@@ -168,11 +153,6 @@ let pr_explanation (e,b,f) =
   let a = if f then str"!" ++ a else a in
     if b then str "[" ++ a ++ str "]" else a
 
-let pr_class_rawexpr = function
-  | FunClass -> str"Funclass"
-  | SortClass -> str"Sortclass"
-  | RefClass qid -> pr_smart_global qid
-
 let pr_option_ref_value = function
   | QualidRefValue id -> pr_reference id
   | StringRefValue s -> qs s
@@ -290,9 +270,6 @@ let pr_decl_notation prc ((loc,ntn),c,scopt) =
   fnl () ++ str "where " ++ qs ntn ++ str " := " ++ prc c ++
   pr_opt (fun sc -> str ": " ++ str sc) scopt
 
-let pr_vbinders l =
-  hv 0 (pr_binders l)
-
 let pr_binders_arg =
   pr_ne_sep spc pr_binders
 
@@ -421,21 +398,6 @@ let pr_grammar_tactic_rule n (_,pil,t) =
     hov 0 (prlist_with_sep sep pr_production_item pil ++
     spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
 
-let pr_box b = let pr_boxkind = function
-  | PpHB n -> str"h" ++ spc() ++ int n
-  | PpVB n -> str"v" ++ spc() ++ int n
-  | PpHVB n -> str"hv" ++ spc() ++ int n
-  | PpHOVB n -> str"hov" ++ spc() ++ int n
-  | PpTB -> str"t"
-in str"<" ++ pr_boxkind b ++ str">"
-
-let pr_paren_reln_or_extern = function
-  | None,L -> str"L"
-  | None,E -> str"E"
-  | Some pprim,Any -> qs pprim
-  | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
-  | _ -> mt()
-
 let pr_statement head (id,(bl,c,guard)) =
   assert (id<>None);
   hov 0
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 62dd94893..c4e378826 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -39,7 +39,6 @@ type object_pr = {
   print_module              : bool -> Names.module_path -> std_ppcmds;
   print_modtype             : module_path -> std_ppcmds;
   print_named_decl          : identifier * constr option * types -> std_ppcmds;
-  print_leaf_entry          : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
@@ -457,11 +456,6 @@ let gallina_print_library_entry with_values ent =
     | (_,Lib.FrozenState _) ->
 	None
 
-let gallina_print_leaf_entry with_values c =
-  match gallina_print_leaf_entry with_values c with
-    | None    -> mt ()
-    | Some pp -> pp ++ fnl()
-
 let gallina_print_context with_values =
   let rec prec n = function
     | h::rest when n = None or Option.get n > 0 ->
@@ -487,7 +481,6 @@ let default_object_pr = {
   print_module              = gallina_print_module;
   print_modtype             = gallina_print_modtype;
   print_named_decl          = gallina_print_named_decl;
-  print_leaf_entry          = gallina_print_leaf_entry;
   print_library_entry       = gallina_print_library_entry;
   print_context             = gallina_print_context;
   print_typed_value_in_env  = gallina_print_typed_value_in_env;
@@ -504,7 +497,6 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x
 let print_module x  = !object_pr.print_module  x
 let print_modtype x = !object_pr.print_modtype x
 let print_named_decl x = !object_pr.print_named_decl x
-let print_leaf_entry x = !object_pr.print_leaf_entry x
 let print_library_entry x = !object_pr.print_library_entry x
 let print_context x = !object_pr.print_context x
 let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x
@@ -583,16 +575,6 @@ let print_full_pure_context () =
    assume that the declaration of constructors and eliminations
    follows the definition of the inductive type *)
 
-let list_filter_vec f vec =
-  let rec frec n lf =
-    if n < 0 then lf
-    else if f vec.(n) then
-      frec (n-1) (vec.(n)::lf)
-    else
-      frec (n-1) lf
-  in
-  frec (Array.length vec -1) []
-
 (* This is designed to print the contents of an opened section *)
 let read_sec_context r =
   let loc,qid = qualid_of_reference r in
@@ -692,15 +674,6 @@ let print_impargs ref =
   (if has_impl then print_impl_args impl
    else (str "No implicit arguments" ++ fnl ()))
 
-let unfold_head_fconst =
-  let rec unfrec k = match kind_of_term k with
-    | Const cst -> constant_value (Global.env ()) cst
-    | Lambda (na,t,b) -> mkLambda (na,t,unfrec b)
-    | App (f,v) -> appvect (unfrec f,v)
-    | _ -> k
-  in
-  unfrec
-
 (* for debug *)
 let inspect depth =
   print_context false (Some depth) (Lib.contents_after None)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index a7820e034..842fc4e89 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -74,7 +74,6 @@ type object_pr = {
   print_module              : bool -> Names.module_path -> std_ppcmds;
   print_modtype             : module_path -> std_ppcmds;
   print_named_decl          : identifier * constr option * types -> std_ppcmds;
-  print_leaf_entry          : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 5d6837e13..34637b1e8 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -242,18 +242,6 @@ let pr_context_of env = match Flags.print_hyps_limit () with
 
 (* display goal parts (Proof mode) *)
 
-let pr_restricted_named_context among env =
-  hv 0 (fold_named_context
-	  (fun env ((id,_,_) as d) pps ->
-	     if true || Idset.mem id among then
-	       pps ++
-		 fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++
-		 pr_var_decl env d
-	     else
-	       pps)
-          env ~init:(mt ()))
-
-
 let pr_predicate pr_elt (b, elts) =
   let pr_elts = prlist_with_sep spc pr_elt elts in
     if b then
@@ -269,13 +257,6 @@ let pr_transparent_state (ids, csts) =
   hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
 	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
 
-let pr_subgoal_metas metas env=
-  let pr_one (meta,typ) =
-    str "?" ++ int meta ++ str " : " ++
-      hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++
-      str (emacs_str (String.make 1 (Char.chr 253)) "") in
-    hv 0 (prlist_with_sep mt pr_one metas)
-
 (* display complete goal *)
 let default_pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in