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, 11 insertions, 11 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 25579a878f..e40a8a2737 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -816,7 +816,7 @@ let pivot v (c1,p1) (c2,p2) =
 	    
 exception FoundProof of  prf_rule
 
-let rec simpl_sys sys = 
+let simpl_sys sys = 
   List.fold_left (fun acc (c,p) -> 
 		    match check_sat (c,p) with
 		    | Tauto -> acc
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 2ce7b72403..beb7b4819c 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -574,7 +574,7 @@ struct
 
   let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
 
-  let rec dump_n x =
+  let dump_n x =
    match x with
     | Mc.N0 -> Lazy.force coq_N0
     | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
@@ -587,12 +587,12 @@ struct
 
   let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
 
-  let rec pp_n o x =  output_string o  (string_of_int (CoqToCaml.n x))
+  let pp_n o x =  output_string o  (string_of_int (CoqToCaml.n x))
 
   let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
    Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
 
-  let rec parse_z term =
+  let parse_z term =
    let (i,c) = get_left_construct term in
     match i with
      | 1 -> Mc.Z0
@@ -777,7 +777,7 @@ struct
         Printf.fprintf o "0" in
     pp_cone o e
 
-  let rec dump_op = function
+  let dump_op = function
    | Mc.OpEq-> Lazy.force coq_OpEq
    | Mc.OpNEq-> Lazy.force coq_OpNEq
    | Mc.OpLe -> Lazy.force coq_OpLe
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 564126d24c..0537cdbe8b 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1499,7 +1499,7 @@ module N =
   
   (** val eqb : n -> n -> bool **)
   
-  let rec eqb n0 m =
+  let eqb n0 m =
     match n0 with
     | N0 ->
       (match m with
@@ -1693,7 +1693,7 @@ module N =
   
   (** val ldiff : n -> n -> n **)
   
-  let rec ldiff n0 m =
+  let ldiff n0 m =
     match n0 with
     | N0 -> N0
     | Npos p ->
@@ -2205,7 +2205,7 @@ module Z =
   
   (** val eqb : z -> z -> bool **)
   
-  let rec eqb x y =
+  let eqb x y =
     match x with
     | Z0 ->
       (match y with
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ccbf0406ef..240c29e0ff 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -89,7 +89,7 @@ let list_try_find f =
   in
   try_find_f
 
-let rec list_fold_right_elements f l =
+let list_fold_right_elements f l =
   let rec aux = function
     | [] -> invalid_arg "list_fold_right_elements"
     | [x] -> x
@@ -142,7 +142,7 @@ let rec rec_gcd_list c l  =
   | [] -> c
   | e::l -> rec_gcd_list (gcd_big_int  c (numerator e)) l
 
-let rec gcd_list l =
+let gcd_list l =
  let res = rec_gcd_list zero_big_int l in
   if compare_big_int res zero_big_int = 0
   then unit_big_int else res
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 36b05a7258..1f7c083e22 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -315,7 +315,7 @@ module Vect =
 	if Big_int.compare_big_int res Big_int.zero_big_int = 0
 	then Big_int.unit_big_int else res
 
-    let rec mul z t =
+    let mul z t =
       match z with
 	| Int 0 -> []
 	| Int 1 -> t