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

4 files changed, 5 insertions, 5 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4a5634673..7e400a332 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -692,7 +692,7 @@ let warn_install_at_root_directory
 
 let check_overlapping_include (_,inc_r) =
   let pwd = Sys.getcwd () in
-  let rec aux = function
+  let aux = function
     | [] -> ()
     | (pdir,_,abspdir)::l ->
 	if not (is_prefix pwd abspdir) then
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4
index 1a9b9c73f..42d3f8f0a 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml4
@@ -122,7 +122,7 @@ let insert texfile coq_output result =
   let next_block k =
     if !last_read = "" then last_read := input_line c_coq;
     (* skip k prompts *)
-    for i = 1 to k do
+    for _i = 1 to k do
       last_read := remove_prompt !last_read;
     done;
     (* read and return the following lines until a prompt is found *)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 45f8e34b1..a8c108f4e 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -20,7 +20,7 @@ let option_D = ref false
 let option_w = ref false
 let option_sort = ref false
 
-let rec warning_mult suf iter =
+let warning_mult suf iter =
   let tab = Hashtbl.create 151 in
   let check f d =
     begin try
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index dc38d3bce..86a5b0cbe 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -566,7 +566,7 @@ module Html = struct
           printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true)
     end
 
-  let indentation n = for i = 1 to n do printf "&nbsp;" done
+  let indentation n = for _i = 1 to n do printf "&nbsp;" done
 
   let line_break () = printf "<br/>\n"
 
@@ -1128,7 +1128,7 @@ module Raw = struct
   let stop_quote () = printf "\""
 
   let indentation n =
-      for i = 1 to n do printf " " done
+      for _i = 1 to n do printf " " done
 
   let keyword s loc = raw_ident s
   let ident s loc = raw_ident s