From 18ebb3f525a965358d96eab7df493450009517b5 Mon Sep 17 00:00:00 2001 From: regisgia Date: Fri, 14 Sep 2012 09:52:38 +0000 Subject: The new ocaml compiler (4.00) has a lot of very cool warnings, especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun.ml | 4 ++-- plugins/funind/merge.ml | 8 ++++---- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 567bdcd6ef..cb41de283a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -423,7 +423,7 @@ let generate_functional_principle exception Not_Rec let get_funs_constant mp dp = - let rec get_funs_constant const e : (Names.constant*int) array = + let get_funs_constant const e : (Names.constant*int) array = match kind_of_term ((strip_lam e)) with | Fix((_,(na,_,_))) -> Array.mapi diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 5b9bf44c3b..0ad8bc5e6d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -188,7 +188,7 @@ let build_newrecursive l = build_newrecursive l' (* Checks whether or not the mutual bloc is recursive *) -let rec is_rec names = +let is_rec names = let names = List.fold_right Idset.add names Idset.empty in let check_id id names = Idset.mem id names in let rec lookup names = function @@ -562,7 +562,7 @@ let decompose_prod_n_assum_constr_expr = open Constrexpr open Topconstr -let rec make_assoc = List.fold_left2 (fun l a b -> +let make_assoc = List.fold_left2 (fun l a b -> match a, b with |(_,Name na), (_, Name id) -> (na, id)::l |_,_ -> l diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 6fff88fd88..b848d77a72 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -570,7 +570,7 @@ let rec merge_rec_hyps shift accrec | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable -let rec build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift = +let build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift = List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec @@ -761,7 +761,7 @@ let merge_constructor_id id1 id2 shift:identifier = (** [merge_constructors lnk shift avoid] merges the two list of constructor [(name*type)]. These are translated to glob_constr first, each of them having distinct var names. *) -let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) +let merge_constructors (shift:merge_infos) (avoid:Idset.t) (typcstr1:(identifier * glob_constr) list) (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list = List.flatten @@ -779,7 +779,7 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t) (** [merge_inductive_body lnk shift avoid oib1 oib2] merges two inductive bodies [oib1] and [oib2], linking with [lnk], params info in [shift], avoiding identifiers in [avoid]. *) -let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) +let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (oib2:one_inductive_body) = (* building glob_constr type of constructors *) let mkrawcor nme avoid typ = @@ -813,7 +813,7 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) [lnk]. [shift] information on parameters of the new inductive. For the moment, inductives are supposed to be non mutual. *) -let rec merge_mutual_inductive_body +let merge_mutual_inductive_body (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) = (* Mutual not treated, we take first ind body of each. *) merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0) -- cgit v1.2.3