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

8 files changed, 3 insertions, 64 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 12b734e563..70f2f6b64a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -30,9 +30,7 @@ open Coercion.Default
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_hyps = Refiner.pf_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
-let pf_concl gls = Goal.V82.concl (Refiner.project gls) (sig_it gls)
 
 (******************************************************************)
 (* Clausal environments *)
@@ -144,9 +142,6 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_rename_from_n gls n (c,t) =
-  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t)
-
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
 (******************************************************************)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 6438f5855f..593ef0b329 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -694,27 +694,6 @@ type variable_proof_status = ProofVar | SectionVar of identifier
 
 type proof_variable = name * variable_proof_status
 
-let subst_proof_vars =
-  let rec aux p vars =
-    let _,subst =
-      List.fold_left (fun (n,l) var ->
-        let t = match var with
-          | Anonymous,_ -> l
-          | Name id, ProofVar -> (id,mkRel n)::l
-          | Name id, SectionVar id' -> (id,mkVar id')::l in
-        (n+1,t)) (p,[]) vars
-    in replace_vars (List.rev subst)
-  in aux 1
-
-let rec rebind id1 id2 = function
-  | [] -> [Name id2,SectionVar id1]
-  | (na,k as x)::l ->
-      if na = Name id1 then (Name id2,k)::l else
-        let l' = rebind id1 id2 l in
-        if na = Name id2 then (Anonymous,k)::l' else x::l'
-
-let add_proof_var id vl = (Name id,ProofVar)::vl
-
 let proof_variable_index x =
   let rec aux n = function
     | (Name id,ProofVar)::l when x = id -> n
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2f2e2016b5..cafe454851 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -37,7 +37,7 @@ let _ = register_proof_mode standard
 (* Default proof mode, to be set at the beginning of proofs. *)
 let default_proof_mode = ref standard
 
-let set_default_proof_mode = 
+let _ =
   Goptions.declare_string_option {Goptions.
     optsync = true ;
     optname = "default proof mode" ;
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6304564b97..d150f2a38e 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -85,7 +85,7 @@ let discharge_strategy (_,(local,obj)) =
   if local then None else
   map_strategy disch_ref obj
 
-let (inStrategy,outStrategy) =
+let inStrategy =
   declare_object {(default_object "STRATEGY") with
                     cache_function = (fun (_,obj) -> cache_strategy obj);
 		    load_function = (fun _ (_,obj) -> cache_strategy obj);
@@ -211,7 +211,7 @@ let subst_red_expr subs e =
     (Pattern.subst_pattern subs)
     e
 
-let (inReduction,_) =
+let inReduction =
   declare_object
     {(default_object "REDUCTION") with
        cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index b094eea6b4..eeccbd0e52 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -24,29 +24,11 @@ open Logic
 let sig_it x = x.it
 let project x = x.sigma
 
-
-let and_status = List.fold_left (+) 0
-
 (* Getting env *)
 
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
 let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
-(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
-   gives
-   [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ;
-   (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ]
- *)
-
-let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
-                    (l : proof_tree list) =
-  match nl with
-    | [] -> []
-    | h::t ->
-	let m,l = list_chop h l in
-	(List.hd fl m) :: (mapshape t (List.tl fl) l)
-
-
 let abstract_operation syntax semantics =
   semantics
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 49423d3d73..855d2cea7d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -105,14 +105,6 @@ type 'id gclause =
 
 let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
 
-let goal_location_of = function
-| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr ->
-      Some scl
-| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr ->
-    None
-| _ ->
-    error "Not a simple \"in\" clause (one hypothesis or the conclusion)"
-
 type 'constr induction_clause =
   ('constr with_bindings induction_arg list * 'constr with_bindings option *
    (intro_pattern_expr located option * intro_pattern_expr located option))
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e9ae0154ff..116526d617 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -204,10 +204,6 @@ open Pp
 open Tacexpr
 open Rawterm
 
-let rec pr_list f = function
-  | []   -> mt ()
-  | a::l1 -> (f a) ++ pr_list f l1
-
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
   let penv = print_named_context env in
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 3b518f5dbf..1c2fb2787e 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -154,11 +154,6 @@ let db_mc_pattern_success debug =
     msgnl (str "The goal has been successfully matched!" ++ fnl() ++
            str "Let us execute the right-hand side part..." ++ fnl())
 
-let pp_match_pattern env = function
-  | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c)
-  | Subterm (b,o,c) ->
-    Subterm (b,o,(extern_constr_pattern (names_of_rel_context env) c))
-
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
   if debug <> DebugOff & !skip = 0 then