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

4 files changed, 5 insertions, 5 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index ff4f19aad6..a79485d1e2 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -147,7 +147,7 @@ let push_val y = function
 let push_item x v (m,l) =
   (Idmap.add x v m, (x,Idset.empty)::l)
 let mem_q x (m,_) = Idmap.mem x m
-let rec find_q x (m,q) =
+let find_q x (m,q) =
   let v = Idmap.find x m in
   let m' = Idmap.remove x m in
   let rec find accs acc = function
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 6ffc792467..a3e240c8d6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -100,7 +100,7 @@ let _ = Errors.register_handler begin function
   | NoSuchProof -> Errors.error "No such proof."
   | _ -> raise Errors.Unhandled
 end
-let rec extract id l =
+let extract id l =
   let rec aux = function
     | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
     | np::l -> let (np', l) = aux l in (np' , np::l)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index dbb295969d..0e2ac1ddef 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -372,7 +372,7 @@ let list_of_sensitive s k env =
   with e when catchable_exception e ->
     tclZERO e env
 
-let rec tclGOALBIND s k = 
+let tclGOALBIND s k = 
   (* spiwack: the first line ensures that the value returned by the tactic [k] will
       not "escape its scope". *)
   let k a = tclBIND (k a) here_s in
@@ -380,7 +380,7 @@ let rec tclGOALBIND s k =
     tclDISPATCHGEN Goal.null Goal.plus tacs
   end
 
-let rec tclGOALBINDU s k = 
+let tclGOALBINDU s k = 
   tclBIND (list_of_sensitive s k) begin fun tacs ->
     tclDISPATCHGEN () unitK tacs
   end
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 39f1bf2876..49026cc0b9 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -104,7 +104,7 @@ let run_com inst =
 let run ini =
   if not ini then
   begin
-    for i=1 to 2 do
+    for _i = 1 to 2 do
       print_char (Char.chr 8);print_char (Char.chr 13)
     done;
     msg_tac_debug (str "Executed expressions: " ++ int !skipped ++ fnl())