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

2 files changed, 11 insertions, 11 deletions

diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 043c9e517a..b940dee3a4 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -95,12 +95,12 @@ let partitionne s =
 *)
 let add_hist le =
    let n = List.length le in
-   let i=ref 0 in
+   let i = ref 0 in
    List.map (fun (ie,s) ->
-              let h =ref [] in
-              for k=1 to (n-(!i)-1) do pop r0 h; done;
+              let h = ref [] in
+              for _k = 1 to (n - (!i) - 1) do pop r0 h; done;
               pop r1 h;
-              for k=1 to !i do pop r0 h; done;
+              for _k = 1 to !i do pop r0 h; done;
               i:=!i+1;
               {coef=ie;hist=(!h);strict=s})
              le
@@ -151,7 +151,7 @@ let deduce1 s =
 let deduce lie =
    let n = List.length (fst (List.hd lie)) in
    let lie=ref (add_hist lie) in
-   for i=1 to n-1 do
+   for _i = 1 to n - 1 do
       lie:= deduce1 !lie;
    done;
    !lie
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 997a18d730..b45932e57e 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -349,7 +349,7 @@ let is_int x = (x.den)=1
 ;;
 
 (* fraction = couple (num,den) *)
-let rec rational_to_fraction x= (x.num,x.den)
+let rational_to_fraction x= (x.num,x.den)
 ;;
 
 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
@@ -360,7 +360,7 @@ let int_to_real n =
    then get coq_R0
    else
      (let s=ref (get coq_R1) in
-      for i=1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done;
+      for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done;
       if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s)
 ;;
 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
@@ -376,9 +376,9 @@ let rational_to_real x =
 let tac_zero_inf_pos gl (n,d) =
    let tacn=ref (apply (get coq_Rlt_zero_1)) in
    let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for i=1 to n-1 do
+   for _i = 1 to n - 1 do
        tacn:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
-   for i=1 to d-1 do
+   for _i = 1 to d - 1 do
        tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
    (tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
 ;;
@@ -390,9 +390,9 @@ let tac_zero_infeq_pos gl (n,d)=
                  then (apply (get coq_Rle_zero_zero))
                  else (apply (get coq_Rle_zero_1))) in
    let tacd=ref (apply (get coq_Rlt_zero_1)) in
-   for i=1 to n-1 do
+   for  _i = 1 to n - 1 do
        tacn:=(tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
-   for i=1 to d-1 do
+   for _i = 1 to d - 1 do
        tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
    (tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
 ;;