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

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5cdf849ef..976947f2e 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -190,7 +190,7 @@ let make_inv_predicate env sigma indf realargs id status concl =
    and introduces generalized hypotheis.
    Precondition: t=(mkVar id) *)
 
-let rec dependent_hyps id idlist gl =
+let dependent_hyps id idlist gl =
   let rec dep_rec =function
     | [] -> []
     | (id1,_,_)::l ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bf494ef36..459236fe5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1455,7 +1455,7 @@ let rec message_of_value gl = function
   | VRec _ | VRTactic _ | VFun _ -> str "<tactic>"
   | VList l -> prlist_with_sep spc (message_of_value gl) l
 
-let rec interp_message_token ist gl = function
+let interp_message_token ist gl = function
   | MsgString s -> str s
   | MsgInt n -> int n
   | MsgIdent (loc,id) ->
@@ -1464,7 +1464,7 @@ let rec interp_message_token ist gl = function
 	with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in
       message_of_value gl v
 
-let rec interp_message_nl ist gl = function
+let interp_message_nl ist gl = function
   | [] -> mt()
   | l -> prlist_with_sep spc (interp_message_token ist gl) l ++ fnl()
 
@@ -2016,7 +2016,7 @@ and interp_match_goal ist goal lz lr lmr =
   let hyps = if lr then List.rev hyps else hyps in
   let concl = pf_concl goal in
   let env = pf_env goal in
-  let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
+  let apply_goal_sub app ist (id,c) csr mt mhyps hyps =
     let rec match_next_pattern find_next () =
       let (lgoal,ctxt,find_next') = find_next () in
       let lctxt = give_context ctxt id in
@@ -2209,7 +2209,7 @@ and interp_genarg_var_list1 ist gl x =
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
-  let rec apply_match_subterm app ist (id,c) csr mt =
+  let apply_match_subterm app ist (id,c) csr mt =
     let rec match_next_pattern find_next () =
       let (lmatch,ctxt,find_next') = find_next () in
       let lctxt = give_context ctxt id in
@@ -2597,7 +2597,7 @@ and interp_atomic ist gl tac =
       abstract_extended_tactic opn args (tac args)
   | TacAlias (loc,s,l,(_,body)) -> fun gl ->
     let evdref = ref gl.sigma in
-    let rec f x = match genarg_tag x with
+    let f x = match genarg_tag x with
     | IntArgType ->
         VInteger (out_gen globwit_int x)
     | IntOrVarArgType ->
@@ -3102,7 +3102,7 @@ let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj =
      subst_function = subst_md;
      classify_function = classify_md}
 
-let rec split_ltac_fun = function
+let split_ltac_fun = function
   | TacFun (l,t) -> (l,t)
   | t -> ([],t)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2d0d2d8b5..895b6dc35 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -49,7 +49,7 @@ open Miscops
 
 exception Bound
 
-let rec nb_prod x =
+let nb_prod x =
   let rec count n c =
     match kind_of_term c with
         Prod(_,_,t) -> count (n+1) t
@@ -101,7 +101,7 @@ let string_of_inductive c =
   | _ -> raise Bound
   with Bound -> error "Bound head variable."
 
-let rec head_constr_bound t =
+let head_constr_bound t =
   let t = strip_outer_cast t in
   let _,ccl = decompose_prod_assum t in
   let hd,args = decompose_app ccl in
@@ -1535,7 +1535,7 @@ let generalize_dep ?(with_let=false) c gl =
   let env = pf_env gl in
   let sign = pf_hyps gl in
   let init_ids = ids_of_named_context (Global.named_context()) in
-  let rec seek d toquant =
+  let seek d toquant =
     if List.exists (fun (id,_,_) -> occur_var_in_decl env id d) toquant
       or dependent_in_decl c d then
       d::toquant