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

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index d5efb5cef..e0b27a2f5 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -764,7 +764,7 @@ let slice i a q =
 
 (* sugar strategy *)
 
-let rec addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat deconne *)
+let addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat deconne *)
 			  
 let addSsugar x l =
   if !sugar_flag
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 97db0f731..4cac90713 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -420,7 +420,7 @@ let pol_sparse_to_term n2 p =
   aux p
 
 
-let rec remove_list_tail l i =
+let remove_list_tail l i =
   let rec aux l i =
     if l=[]
     then []
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index e030c2822..071df5cf7 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -160,7 +160,7 @@ let rec max_var_pol2 p =
       Pint _ -> 0
     |Prec(v,c)-> Array.fold_right (fun q m -> max (max_var_pol2 q) m) c v
 
-let rec max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
+let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
 
 (* equality between polynomials *)
 
@@ -181,7 +181,7 @@ let rec equal p q =
    if constant, returns the coefficient
 *)
 
-let rec norm p = match p with
+let norm p = match p with
     Pint _ -> p
   |Prec (x,a)->
      let d = (Array.length a -1) in
@@ -198,7 +198,7 @@ let rec norm p = match p with
 
 
 (* degree in v, v >= max var of p *)
-let rec deg v p =
+let deg v p =
   match p with
       Prec(x,p1) when x=v -> Array.length p1 -1
     |_ -> 0
@@ -276,7 +276,7 @@ let rec vars=function
 
 
 (* multiply p by v^n, v >= max_var p *)
-let rec multx n v p =
+let multx n v p =
   match p with
       Prec (x,p1) when x=v -> let p2= Array.create ((Array.length p1)+n) (Pint coef0) in
         for i=0 to (Array.length p1)-1 do
@@ -314,7 +314,7 @@ let rec multP p q =
 
 
 (* derive p with variable v, v >= max_var p *)
-let rec deriv v p =
+let deriv v p =
   match p with
       Pint a -> Pint coef0
     | Prec(x,p1) when x=v ->
@@ -656,7 +656,7 @@ and gcd_sub_res_rec p q s c d x =
 
 and lazard_power c s d x =
   let res = ref c in
-    for i=1 to d-1 do
+    for _i = 1 to d - 1 do
       res:= div_pol ((!res)@@c) s x;
     done;
     !res