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

11 files changed, 32 insertions, 35 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index d307de4d94..9012d93227 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -100,7 +100,7 @@ let normalize_neg n =
    input: an array with first bloc in [-base;base[ and others in [0;base[
    output: a canonical array *)
 
-let rec normalize n =
+let normalize n =
   if Array.length n = 0 then n
   else if n.(0) = -1 then normalize_neg n
   else if n.(0) = 0 then normalize_pos n
@@ -172,7 +172,7 @@ let sub n m =
   if d >= 0 then sub_to (Array.copy n) m d
   else let r = neg m in add_to r n (Array.length r - Array.length n)
 
-let rec mult m n =
+let mult m n =
   if m = zero or n = zero then zero else
   let l = Array.length m + Array.length n in
   let r = Array.create l 0 in
diff --git a/lib/dnet.ml b/lib/dnet.ml
index 0562cc40b3..a9e1e97e36 100644
--- a/lib/dnet.ml
+++ b/lib/dnet.ml
@@ -169,13 +169,13 @@ struct
   (* Sets with a neutral element for inter *)
   module OSet (S:Set.S) = struct
     type t = S.t option
-    let union s1 s2 = match s1,s2 with
+    let union s1 s2 : t = match s1,s2 with
       | (None, _ | _, None) -> None
       | Some a, Some b -> Some (S.union a b)
-    let inter s1 s2 = match s1,s2 with
+    let inter s1 s2 : t = match s1,s2 with
       | (None, a | a, None) -> a
       | Some a, Some b -> Some (S.inter a b)
-    let is_empty = function 
+    let is_empty : t -> bool = function 
       | None -> false
       | Some s -> S.is_empty s
     (* optimization hack: Not_found is catched in fold_pattern *)
diff --git a/lib/explore.ml b/lib/explore.ml
index 1c8776a4a9..90258b0e55 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -21,7 +21,7 @@ module Make = functor(S : SearchProblem) -> struct
 
   type position = int list
 
-  let msg_with_position p pp =
+  let msg_with_position (p : position) pp =
     let rec pp_rec = function
       | [] -> mt ()
       | [i] -> int i
@@ -58,7 +58,7 @@ module Make = functor(S : SearchProblem) -> struct
 
   let empty = [],[]
 
-  let push x (h,t) = (x::h,t)
+  let push x (h,t) : _ queue = (x::h,t)
 
   let pop = function
     | h, x::t -> x, (h,t)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 5f4738dcf4..7c2897be09 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -60,7 +60,6 @@ module Make(X:Comp) =
      *)
     module Htbl = Hashtbl.Make(
       struct type t=X.t
-             type u=X.u
              let hash=X.hash
              let equal x1 x2 = (*incr comparaison;*) X.equal x1 x2
       end)
diff --git a/lib/pp.ml b/lib/pp.ml
index 463e3fc3cd..1899b2d3c9 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -71,8 +71,6 @@ type ppcmd = (int*string) ppcmd_token
 
 type std_ppcmds = ppcmd Stream.t
 
-type 'a ppdirs = 'a ppdir_token Stream.t
-
 let is_empty s =
   try Stream.empty s; true with Stream.Failure -> false
 
@@ -175,7 +173,7 @@ let rec eval_ppcmds l =
   Stream.of_list (aux l)
 
 (* In new syntax only double quote char is escaped by repeating it *)
-let rec escape_string s =
+let escape_string s =
   let rec escape_at s i =
     if i<0 then s
     else if s.[i] == '"' then
diff --git a/lib/profile.ml b/lib/profile.ml
index 2472d75df7..9002972d9e 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -221,7 +221,7 @@ let loops = 10000
 let time_overhead_A_D () =
   let e = create_record () in
   let before = get_time () in
-  for i=1 to loops do
+  for _i = 1 to loops do
     (* This is a copy of profile1 for overhead estimation *)
     let dw = dummy_spent_alloc () in
     match !dummy_stack with [] -> assert false | p::_ ->
@@ -245,7 +245,7 @@ let time_overhead_A_D () =
   done;
   let after = get_time () in
   let beforeloop =  get_time () in
-  for i=1 to loops do () done;
+  for _i = 1 to loops do () done;
   let afterloop = get_time () in
   float_of_int ((after - before) - (afterloop - beforeloop))
   /. float_of_int loops
@@ -253,7 +253,7 @@ let time_overhead_A_D () =
 let time_overhead_B_C () =
   let dummy_x = 0 in
   let before = get_time () in
-  for i=1 to loops do
+  for _i = 1 to loops do
     try
       dummy_last_alloc := get_alloc ();
       let _r = dummy_f dummy_x in
@@ -264,7 +264,7 @@ let time_overhead_B_C () =
   done;
   let after = get_time () in
   let beforeloop =  get_time () in
-  for i=1 to loops do () done;
+  for _i = 1 to loops do () done;
   let afterloop = get_time () in
   float_of_int ((after - before) - (afterloop - beforeloop))
   /. float_of_int loops
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 8f859b47e0..b7fe9184e4 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -101,7 +101,7 @@ let rec map f t = match t with
   | Node (a,sons) -> Node (f a, Array.map (map f) sons)
   | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
 
-let rec smartmap f t = match t with
+let smartmap f t = match t with
     Param _ -> t
   | Node (a,sons) ->
       let a'=f a and sons' = Util.array_smartmap (map f) sons in
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 0f19badf49..04405ac1bf 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -508,7 +508,7 @@ let pr_option_value = function
 | StringValue s -> s
 | BoolValue b -> if b then "true" else "false"
 
-let rec pr_setoptions opts =
+let pr_setoptions opts =
   let map (key, v) =
     let key = String.concat " " key in
     key ^ " := " ^ (pr_option_value v)
diff --git a/lib/system.ml b/lib/system.ml
index bfa46c4b3b..e721b1f654 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -58,7 +58,7 @@ let where_in_path ?(warn=true) path filename =
 	  then (lpe,f) :: search rem
 	  else search rem
     | [] -> [] in
-  let rec check_and_warn l =
+  let check_and_warn l =
     match l with
       | [] -> raise Not_found
       | (lpe, f) :: l' ->
diff --git a/lib/util.ml b/lib/util.ml
index ddc88e83b1..1365f53cef 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -548,7 +548,7 @@ let rec list_fold_left3 f accu l1 l2 l3 =
      a1
      []] *)
 
-let rec list_fold_right_and_left f l hd =
+let list_fold_right_and_left f l hd =
   let rec aux tl = function
     | [] -> hd
     | a::l -> let hd = aux (a::tl) l in f hd a tl
@@ -636,7 +636,7 @@ let list_uniquize l =
     | [] -> List.rev acc
   in aux [] l
 
-let rec list_distinct l =
+let list_distinct l =
   let visited = Hashtbl.create 23 in
   let rec loop = function
     | h::t ->
@@ -774,7 +774,7 @@ let rec list_skipn n l = match n,l with
   | _, [] -> failwith "list_skipn"
   | n, _::l -> list_skipn (pred n) l
 
-let rec list_skipn_at_least n l =
+let list_skipn_at_least n l =
   try list_skipn n l with Failure _ -> []
 
 let list_prefix_of prefl l =
@@ -852,7 +852,7 @@ let list_union_map f l acc =
    [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
    and so on if there are more elements in the lists. *)
 
-let rec list_cartesian op l1 l2 =
+let list_cartesian op l1 l2 =
   list_map_append (fun x -> List.map (op x) l2) l1
 
 (* [list_cartesians] is an n-ary cartesian product: it iterates
@@ -874,12 +874,12 @@ let rec list_combine3 x y z =
   
 (* Keep only those products that do not return None *)
 
-let rec list_cartesian_filter op l1 l2 =
+let list_cartesian_filter op l1 l2 =
   list_map_append (fun x -> list_map_filter (op x) l2) l1
 
 (* Keep only those products that do not return None *)
 
-let rec list_cartesians_filter op init ll =
+let list_cartesians_filter op init ll =
   List.fold_right (list_cartesian_filter op) ll [init]
 
 (* Drop the last element of a list *)
@@ -1217,15 +1217,6 @@ let array_filter_along f filter v =
 let array_filter_with filter v =
   Array.of_list (list_filter_with filter (Array.to_list v))
 
-(* Stream *)
-
-let stream_nth n st =
-  try List.nth (Stream.npeek (n+1) st) n
-  with Failure _ -> raise Stream.Failure
-
-let stream_njunk n st =
-  for i = 1 to n do Stream.junk st done
-
 (* Matrices *)
 
 let matrix_transpose mat =
@@ -1247,7 +1238,7 @@ let iterate f =
   iterate_f
 
 let repeat n f x =
-  for i = 1 to n do f x done
+  let rec loop i = if i <> 0 then (f x; loop (i - 1)) in loop n
 
 let iterate_for a b f x =
   let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
@@ -1258,6 +1249,15 @@ let app_opt f x =
   | Some f -> f x
   | None -> x
 
+(* Stream *)
+
+let stream_nth n st =
+  try List.nth (Stream.npeek (n+1) st) n
+  with Failure _ -> raise Stream.Failure
+
+let stream_njunk n st =
+  repeat n Stream.junk st
+
 (* Delayed computations *)
 
 type 'a delayed = unit -> 'a
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml
index 48ee546cad..0a3b5da47e 100644
--- a/lib/xml_utils.ml
+++ b/lib/xml_utils.ml
@@ -116,7 +116,7 @@ let buffer_attr (n,v) =
 	done;
 	Buffer.add_char tmp '"'
 
-let rec print_attr chan (n, v) =
+let print_attr chan (n, v) =
   Printf.fprintf chan " %s=\"" n;
   let l = String.length v in
   for p = 0 to l-1 do