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

1 files changed, 6 insertions, 6 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4aaf145e5..ed06d6e11 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -594,7 +594,7 @@ let compile name kind =
   in
   loop []
 
-let rec decompile af =
+let decompile af =
   let rec loop = function
     | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r)
     | [] -> Oz af.constant
@@ -685,7 +685,7 @@ let rec shuffle p (t1,t2) =
 	  Oplus(t2,t1)
 	else [],Oplus(t1,t2)
 
-let rec shuffle_mult p_init k1 e1 k2 e2 =
+let shuffle_mult p_init k1 e1 k2 e2 =
   let rec loop p = function
     | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
 	if v1 = v2 then
@@ -742,7 +742,7 @@ let rec shuffle_mult p_init k1 e1 k2 e2 =
   in
   loop p_init (e1,e2)
 
-let rec shuffle_mult_right p_init e1 k2 e2 =
+let shuffle_mult_right p_init e1 k2 e2 =
   let rec loop p = function
     | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
 	if v1 = v2 then
@@ -827,7 +827,7 @@ let rec scalar p n = function
   | Oz i -> [focused_simpl p],Oz(n*i)
   | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
 
-let rec scalar_norm p_init =
+let scalar_norm p_init =
   let rec loop p = function
     | [] -> [focused_simpl p_init]
     | (_::l) ->
@@ -838,7 +838,7 @@ let rec scalar_norm p_init =
   in
   loop p_init
 
-let rec norm_add p_init =
+let norm_add p_init =
   let rec loop p = function
     | [] -> [focused_simpl p_init]
     | _:: l ->
@@ -848,7 +848,7 @@ let rec norm_add p_init =
   in
   loop p_init
 
-let rec scalar_norm_add p_init =
+let scalar_norm_add p_init =
   let rec loop p = function
     | [] -> [focused_simpl p_init]
     | _ :: l ->