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, 5 insertions, 146 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2cbef98e8..18f1d13ea 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -202,75 +202,6 @@ and check_same_fix_binder bl1 bl2 =
 
 let same c d = try check_same_type c d; true with _ -> false
 
-(* Idem for rawconstr *)
-
-let array_iter2 f v1 v2 =
-  List.iter2 f (Array.to_list v1) (Array.to_list v2)
-
-let rec same_patt p1 p2 =
-  match p1, p2 with
-      PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar"
-    | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) ->
-        if c1<>c2 || al1 <> al2 then failwith "PatCstr";
-        List.iter2 same_patt pl1 pl2
-    | _ -> failwith "same_patt"
-
-let rec same_raw c d =
-  match c,d with
-   | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef"
-   | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
-   | REvar(_,e1,a1), REvar(_,e2,a2) ->
-       if e1 <> e2 then failwith "REvar";
-       Option.iter2(List.iter2 same_raw) a1 a2
-  | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
-  | RApp(_,f1,a1), RApp(_,f2,a2) ->
-      List.iter2 same_raw (f1::a1) (f2::a2)
-  | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) ->
-      if na1 <> na2 then failwith "RLambda";
-      same_raw t1 t2; same_raw m1 m2
-  | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) ->
-      if na1 <> na2 then failwith "RProd";
-      same_raw t1 t2; same_raw m1 m2
-  | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
-      if na1 <> na2 then failwith "RLetIn";
-      same_raw t1 t2; same_raw m1 m2
-  | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) ->
-      List.iter2
-        (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
-          same_raw t1 t2;
-          if al1 <> al2 then failwith "RCases";
-          Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
-            if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
-      List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
-        List.iter2 same_patt pl1 pl2;
-        same_raw b1 b2) b1 b2
-  | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) ->
-      if nl1<>nl2 then failwith "RLetTuple";
-      same_raw b1 b2;
-      same_raw c1 c2
-  | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) ->
-      same_raw b1 b2; same_raw t1 t2; same_raw e1 e2
-  | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
-      if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
-      array_iter2
-        (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) ->
-          if na1<>na2 then failwith "RRec";
-          Option.iter2 same_raw bd1 bd2;
-          same_raw ty1 ty2)) bl1 bl2;
-      array_iter2 same_raw ty1 ty2;
-      array_iter2 same_raw def1 def2
-  | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort"
-  | RHole _, _ -> ()
-  | _, RHole _ -> ()
-  | RCast(_,c1,_),r2 -> same_raw c1 r2
-  | r1, RCast(_,c2,_) -> same_raw r1 c2
-  | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
-  | _ -> failwith "same_raw"
-
-let same_rawconstr c d =
-  try same_raw c d; true
-  with Failure _ | Invalid_argument _ -> false
-
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
@@ -555,11 +486,6 @@ let rec flatten_application = function
   | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l))
   | a -> a
 
-let rec rename_rawconstr_var id0 id1 = function
-    RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1)
-  | RVar(loc,id) when id=id0 -> RVar(loc,id1)
-  | c -> map_rawconstr (rename_rawconstr_var id0 id1) c
-
 (**********************************************************************)
 (* mapping rawterms to numerals (in presence of coercions, choose the *)
 (* one with no delimiter if possible)                                 *)
@@ -964,32 +890,6 @@ let rec raw_of_pat env = function
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
 
-and raw_of_eqn env constr construct_nargs branch =
-  let make_pat x env b ids =
-    let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
-    let id = next_name_away_with_default "x" x avoid in
-    PatVar (dummy_loc,Name id),(Name id)::env,id::ids
-  in
-  let rec buildrec ids patlist env n b =
-    if n=0 then
-      (dummy_loc, ids,
-       [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
-       raw_of_pat env b)
-    else
-      match b with
-	| PLambda (x,_,b) ->
-	    let pat,new_env,new_ids = make_pat x env b ids in
-            buildrec new_ids (pat::patlist) new_env (n-1) b
-
-	| PLetIn (x,_,b) ->
-	    let pat,new_env,new_ids = make_pat x env b ids in
-            buildrec new_ids (pat::patlist) new_env (n-1) b
-
-	| _ ->
-	    error "Unsupported branch in case-analysis while printing pattern."
-  in
-  buildrec [] [] env construct_nargs branch
-
 let extern_constr_pattern env pat =
   extern true (None,[]) Idset.empty (raw_of_pat env pat)
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 3d618b0bc..bb555148f 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -106,11 +106,6 @@ let init_modules = [
   init_dir@["Wf"]
 ]
 
-let coq_id = id_of_string "Coq"
-let init_id = id_of_string "Init"
-let arith_id = id_of_string "Arith"
-let datatypes_id = id_of_string "Datatypes"
-
 let logic_module_name = ["Coq";"Init";"Logic"]
 let logic_module = make_dir logic_module_name
 
@@ -225,8 +220,6 @@ let lazy_logic_constant dir id = lazy (logic_constant dir id)
 let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
 let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl"
 let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
-let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
-let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
 let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
 let coq_eq_sym  = lazy_init_constant ["Logic"] "eq_sym"
 let coq_eq_trans  = lazy_init_constant ["Logic"] "eq_trans"
@@ -248,8 +241,6 @@ let build_coq_eq_refl () = Lazy.force coq_eq_refl
 let build_coq_eq_sym () = Lazy.force coq_eq_sym
 let build_coq_f_equal2 () = Lazy.force coq_f_equal2
 
-let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
-
 let build_coq_inversion_eq_data () =
   let _ = check_required_library logic_module_name in {
   inv_eq = Lazy.force coq_eq_eq;
@@ -261,8 +252,6 @@ let build_coq_inversion_eq_data () =
 let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq"
 let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl"
 let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind"
-let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec"
-let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect"
 let coq_jmeq_sym  = lazy_logic_constant ["JMeq"] "JMeq_sym"
 let coq_jmeq_congr  = lazy_logic_constant ["JMeq"] "JMeq_congr"
 let coq_jmeq_trans  = lazy_logic_constant ["JMeq"] "JMeq_trans"
@@ -298,8 +287,6 @@ let build_coq_sumbool () = Lazy.force coq_sumbool
 let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
 let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
 let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
-let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
-let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
 let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
 let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
 let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans"
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 113b12f23..e7394d70c 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -154,11 +154,6 @@ let dump_constraint ((loc, n), _, _) sec ty =
     | Names.Name id -> dump_definition (loc, id) sec ty
     | Names.Anonymous -> ()
 
-let dump_name (loc, n) sec ty =
-  match n with
-    | Names.Name id -> dump_definition (loc, id) sec ty
-    | Names.Anonymous -> ()
-
 let dump_modref loc mp ty =
   if dump () then
     let (dp, l) = Lib.split_modpath mp in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 0776e63c6..1e97c5178 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -57,7 +57,7 @@ let cache_generalizable_type (_,(local,cmd)) =
 let load_generalizable_type _ (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
     
-let (in_generalizable, _) =
+let in_generalizable =
   declare_object {(default_object "GENERALIZED-IDENT") with
     load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
@@ -203,8 +203,6 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty)
 let rec make_fresh ids env x =
   if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x)
 
-let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-
 let next_name_away_from na avoid =
   match na with
   | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
diff --git a/interp/notation.ml b/interp/notation.ml
index 0395e9bc3..d5e27841a 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -111,13 +111,10 @@ let subst_scope (subst,sc) = sc
 
 open Libobject
 
-let discharge_scope (local,_,_ as o) =
-  if local then None else Some o
-
 let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let (inScope,outScope) =
+let inScope =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
       open_function = open_scope;
@@ -499,7 +496,7 @@ let rebuild_arguments_scope (req,r,l) =
 	let l1,_ = list_chop (List.length l' - List.length l) l' in
 	(req,r,l1@l)
 
-let (inArgumentsScope,outArgumentsScope) =
+let inArgumentsScope =
   declare_object {(default_object "ARGUMENTS-SCOPE") with
       cache_function = cache_arguments_scope;
       load_function = load_arguments_scope;
@@ -622,9 +619,6 @@ let factorize_entries = function
 	  (ntn,[c],[]) l in
       (ntn,l_of_ntn)::rest
 
-let is_ident s = (* Poor analysis *)
-  String.length s <> 0 & is_letter s.[0]
-
 let browse_notation strict ntn map =
   let find =
     if String.contains ntn ' ' then (=) ntn
diff --git a/interp/reserve.ml b/interp/reserve.ml
index ec58e47fa..3bcd6b1e7 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -21,7 +21,7 @@ let reserve_table = ref Idmap.empty
 let cache_reserved_type (_,(id,t)) =
   reserve_table := Idmap.add id t !reserve_table
 
-let (in_reserved, _) =
+let in_reserved =
   declare_object {(default_object "RESERVED-TYPE") with
     cache_function = cache_reserved_type }
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 954485f77..8056ab426 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -62,7 +62,7 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) =
 let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let (in_syntax_constant, out_syntax_constant) =
+let in_syntax_constant =
   declare_object {(default_object "SYNTAXCONSTANT") with
     cache_function = cache_syntax_constant;
     load_function = load_syntax_constant;
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index dc35c47db..cbdb41ea3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -508,8 +508,6 @@ let subst_interpretation subst (metas,pat) =
   let bound = List.map fst metas in
   (metas,subst_aconstr subst bound pat)
 
-let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
-
 (* Pattern-matching rawconstr and aconstr *)
 
 let abstract_return_type_context pi mklam tml rtno =
@@ -528,11 +526,6 @@ let abstract_return_type_context_aconstr =
   abstract_return_type_context pi3
     (fun na c -> ALambda(na,AHole Evd.InternalHole,c))
 
-let rec adjust_scopes = function
-  | _,[] -> []
-  | [],a::args -> (None,a) :: adjust_scopes ([],args)
-  | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args)
-
 exception No_match
 
 let rec alpha_var id1 id2 = function
@@ -586,10 +579,6 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
 	(match_names metas acc na1 na2) patl1 patl2
   | _ -> raise No_match
 
-let adjust_application_n n loc f l =
-  let l1,l2 = list_chop (List.length l - n) l in
-  if l1 = [] then f,l else RApp (loc,f,l1), l2
-
 let glue_letin_with_decls = true
 
 let rec match_iterated_binders islambda decls = function
@@ -947,10 +936,6 @@ let local_binders_loc bll =
   if bll = [] then dummy_loc else
   join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
 
-let occur_var_constr_ref id = function
-  | Ident (loc,id') -> id = id'
-  | Qualid _ -> false
-
 let ids_of_cases_indtype =
   let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
   let rec vars_of = function