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

5 files changed, 8 insertions, 8 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d6b3a9596c..7a40a40297 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -220,7 +220,7 @@ let pos_rel i r sz =
 (* non-terminating instruction (branch, raise, return, appterm)          *)
 (* in front of it.                                                       *)
 
-let rec discard_dead_code cont = cont
+let discard_dead_code cont = cont
 (*function
     [] -> []
   | (Klabel _ | Krestart ) :: _ as cont -> cont
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2c723a8344..f1adb53406 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -317,7 +317,7 @@ let compile_constant_body = Cbytegen.compile_constant_body
 
 exception Hyp_not_found
 
-let rec apply_to_hyp (ctxt,vals) id f =
+let apply_to_hyp (ctxt,vals) id f =
   let rec aux rtail ctxt vals =
     match ctxt, vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
@@ -330,7 +330,7 @@ let rec apply_to_hyp (ctxt,vals) id f =
     | _, _ -> assert false
   in aux [] ctxt vals
 
-let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
+let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   let rec aux ctxt vals =
     match ctxt,vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 7c0b14dce3..a9d4d88325 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -147,7 +147,7 @@ let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver
 let mp_of_delta resolve mp =
  try Deltamap.find_mp mp resolve with Not_found -> mp
 
-let rec find_prefix resolve mp =
+let find_prefix resolve mp =
   let rec sub_mp = function
     | MPdot(mp,l) as mp_sup ->
 	(try Deltamap.find_mp mp_sup resolve
diff --git a/kernel/term.ml b/kernel/term.ml
index 9a25de1bcf..16649b1815 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -108,6 +108,8 @@ type ('constr, 'types) kind_of_term =
    -rectypes of the Caml compiler to be set *)
 type constr = (constr,constr) kind_of_term
 
+type strategy = types option
+
 type existential = existential_key * constr array
 type rec_declaration = name array * constr array * constr array
 type fixpoint = (int array * int) * rec_declaration
@@ -429,7 +431,7 @@ let rec under_casts f c = match kind_of_term c with
 (******************************************************************)
 
 (* flattens application lists throwing casts in-between *)
-let rec collapse_appl c = match kind_of_term c with
+let collapse_appl c = match kind_of_term c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 =
         match kind_of_term (strip_outer_cast f) with
@@ -647,8 +649,6 @@ let rec constr_ord m n=
 
 type types = constr
 
-type strategy = types option
-
 type named_declaration = identifier * constr option * types
 type rel_declaration = name * constr option * types
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9487b6d393..608bcc886c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -95,7 +95,7 @@ let judge_of_variable env id =
 (* Checks if a context of variable can be instantiated by the
    variables of the current env *)
 (* TODO: check order? *)
-let rec check_hyps_inclusion env sign =
+let check_hyps_inclusion env sign =
   Sign.fold_named_context
     (fun (id,_,ty1) () ->
       let ty2 = named_type id env in