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

3 files changed, 7 insertions, 7 deletions

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)