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

11 files changed, 20 insertions, 20 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 33b1e8136..5c3e8fe92 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -183,7 +183,7 @@ let complete_history = glob_pattern_of_partial_history []
 
 (* This is to build glued pattern-matching history and alias bodies *)
 
-let rec pop_history_pattern = function
+let pop_history_pattern = function
   | Continuation (0, l, Top) ->
       Result (List.rev l)
   | Continuation (0, l, MakeConstructor (pci, rh)) ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7418dbc3e..bd23501a8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -75,7 +75,7 @@ let app_opt env evars f t =
 let pair_of_array a = (a.(0), a.(1))
 let make_name s = Name (id_of_string s)
 
-let rec disc_subset x =
+let disc_subset x =
   match kind_of_term x with
   | App (c, l) ->
       (match kind_of_term c with
@@ -102,7 +102,7 @@ let lift_args n sign =
   in
     liftrec (List.length sign) sign
 
-let rec mu env isevars t =
+let mu env isevars t =
   let rec aux v =
     let v' = hnf env !isevars v in
       match disc_subset v' with
@@ -133,7 +133,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
       | [(na,b,t)], c -> (na,t), c
       | _ -> raise NoSubtacCoercion
     in
-    let rec coerce_application typ typ' c c' l l' =
+    let coerce_application typ typ' c c' l l' =
       let len = Array.length l in
       let rec aux tele typ typ' i co =
 	if i < len then
@@ -211,7 +211,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		       pair_of_array l, pair_of_array l'
 		     in
 		     let c1 = coerce_unify env a a' in
-		     let rec remove_head a c =
+		     let remove_head a c =
 		       match kind_of_term c with
 		       | Lambda (n, t, t') -> c, t'
 			   (*| Prod (n, t, t') -> t'*)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 89e3e5fbb..6329a62b9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -298,7 +298,7 @@ let it_destRLambda_or_LetIn_names n c =
       | GLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
       | _ ->
           (* eta-expansion *)
-	  let rec next l =
+	  let next l =
 	    let x = next_ident_away (id_of_string "x") l in
 	    (* Not efficient but unusual and no function to get free glob_vars *)
 (* 	    if occur_glob_constr x c then next (x::l) else x in *)
@@ -557,7 +557,7 @@ and detype_binder isgoal bk avoid env na ty c =
   | BLambda -> GLambda (dl, na',Explicit,detype false avoid env ty, r)
   | BLetIn -> GLetIn (dl, na',detype false avoid env ty, r)
 
-let rec detype_rel_context where avoid env sign =
+let detype_rel_context where avoid env sign =
   let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function
   | [] -> []
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f4c3a1bb4..90492d50c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -505,7 +505,7 @@ let expand_alias_once aliases x =
   | []  -> None
   | l -> Some (list_last l)
 
-let rec expansions_of_var aliases x =
+let expansions_of_var aliases x =
   match get_alias_chain_of aliases x with
   | [] -> [x]
   | a::_ as l when isRel a || isVar a -> x :: List.rev l
@@ -689,7 +689,7 @@ module Constrhash = Hashtbl.Make
 	  let hash = hash_constr
    end)
 
-let rec constr_list_distinct l =
+let constr_list_distinct l =
   let visited = Constrhash.create 23 in
   let rec loop = function
     | h::t ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 551ede05c..1c7302fe0 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -73,7 +73,7 @@ let mkAppliedInd (IndType ((ind,params), realargs)) =
 
 (* Does not consider imbricated or mutually recursive types *)
 let mis_is_recursive_subset listind rarg =
-  let rec one_is_rec rvec =
+  let one_is_rec rvec =
     List.exists
       (fun ra ->
         match dest_recarg ra with
@@ -242,7 +242,7 @@ let substnl_rel_context subst n sign =
 
 let substl_rel_context subst = substnl_rel_context subst 0
 
-let rec instantiate_context sign args =
+let instantiate_context sign args =
   let rec aux subst = function
   | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args)
   | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args)
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 32c8ca33d..fc84c8efa 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -26,7 +26,7 @@ open Termops
 (**********************************************************************)
 (* Globality of identifiers *)
 
-let rec is_imported_modpath mp =
+let is_imported_modpath mp =
   let current_mp,_ = Lib.current_prefix() in
     match mp with
       | MPfile dp ->
@@ -313,7 +313,7 @@ let compute_displayed_let_name_in flags avoid na c =
   let fresh_id = next_name_for_display flags na avoid in
   (Name fresh_id, fresh_id::avoid)
 
-let rec rename_bound_vars_as_displayed avoid env c =
+let rename_bound_vars_as_displayed avoid env c =
   let rec rename avoid env c =
     match kind_of_term c with
     | Prod (na,c1,c2)  ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index edbacbebe..bdc6cb72a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -558,7 +558,7 @@ let nf_betadeltaiota env sigma =
    du type checking :
      (fun x => x + x) M
 *)
-let rec whd_betaiota_preserving_vm_cast env sigma t =
+let whd_betaiota_preserving_vm_cast env sigma t =
    let rec stacklam_var subst t stack =
      match (decomp_stack stack,kind_of_term t) with
      | Some (h,stacktl), Lambda (_,_,c) ->
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4a80f82b7..ae4e3b2f8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1061,7 +1061,7 @@ let reduce_to_ind_gen allow_product env sigma t =
 let reduce_to_quantified_ind x = reduce_to_ind_gen true x
 let reduce_to_atomic_ind x = reduce_to_ind_gen false x
 
-let rec find_hnf_rectype env sigma t =
+let find_hnf_rectype env sigma t =
   let ind,t = reduce_to_atomic_ind env sigma t in
   ind, snd (decompose_app t)
 
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml
index 153431093..49c93ffdd 100644
--- a/pretyping/term_dnet.ml
+++ b/pretyping/term_dnet.ml
@@ -53,7 +53,7 @@ struct
   type dconstr = dconstr t
 
   (* debug *)
-  let rec pr_dconstr f : 'a t -> std_ppcmds = function
+  let pr_dconstr f : 'a t -> std_ppcmds = function
     | DRel -> str "*"
     | DSort -> str "Sort"
     | DRef _ -> str "Ref"
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 25e4c25ce..9bd539abc 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -219,7 +219,7 @@ let push_named_rec_types (lna,typarray,_) env =
   Array.fold_left
     (fun e assum -> push_named assum e) env ctxt
 
-let rec lookup_rel_id id sign =
+let lookup_rel_id id sign =
   let rec lookrec = function
     | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
     | (n, (Name id',b,t)::l)  -> if id' = id then (n,b,t) else lookrec (n+1,l)
@@ -839,7 +839,7 @@ let add_name n nl = n::nl
 let lookup_name_of_rel p names =
   try List.nth names (p-1)
   with Invalid_argument _ | Failure _ -> raise Not_found
-let rec lookup_rel_of_name id names =
+let lookup_rel_of_name id names =
   let rec lookrec n = function
     | Anonymous :: l  -> lookrec (n+1) l
     | (Name id') :: l -> if id' = id then n else lookrec (n+1) l
@@ -1056,7 +1056,7 @@ let rec mem_named_context id = function
   | [] -> false
 
 let clear_named_body id env =
-  let rec aux _ = function
+  let aux _ = function
   | (id',Some c,t) when id = id' -> push_named (id,None,t)
   | d -> push_named d in
   fold_named_context aux env ~init:(reset_context env)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8c537d369..ebb30bf35 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -73,7 +73,7 @@ let e_check_branch_types env evdref ind cj (lfj,explft) =
       error_ill_formed_branch env cj.uj_val (ind,i+1) lfj.(i).uj_type explft.(i)
   done
 
-let rec max_sort l =
+let max_sort l =
   if List.mem InType l then InType else
   if List.mem InSet l then InSet else InProp