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

28 files changed, 65 insertions, 65 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 26fd43a68..0970717ed 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -68,7 +68,7 @@ module ST=struct
     with
 	Not_found -> ()
 
-  let rec delete_set st s = Intset.iter (delete st) s
+  let delete_set st s = Intset.iter (delete st) s
 
 end
 
@@ -781,7 +781,7 @@ let make_fun_table state =
     !funtab
 
 
-let rec do_match state res pb_stack =
+let do_match state res pb_stack =
   let mp=Stack.pop pb_stack in
     match mp.mp_stack with
 	[] ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 07813741c..2042f9b05 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -179,7 +179,7 @@ let litteral_of_constr env sigma term=
 
 (* store all equalities from the context *)
 
-let rec make_prb gls depth additionnal_terms =
+let make_prb gls depth additionnal_terms =
   let env=pf_env gls in
   let sigma=sig_sig gls in
   let state = empty depth gls in
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 5b1f15480..e387b31a5 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -138,7 +138,7 @@ let rec intern_bare_proof_instr globs = function
   | Pcast (id,typ) ->
       Pcast (id,intern_constr globs typ)
 
-let rec intern_proof_instr globs instr=
+let intern_proof_instr globs instr=
   {emph = instr.emph;
    instr = intern_bare_proof_instr globs instr.instr}
 
@@ -467,7 +467,7 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu
   | Pcast (id,typ) ->
       Pcast(id,interp_constr true sigma env typ)
 
-let rec interp_proof_instr info sigma env instr=
+let interp_proof_instr info sigma env instr=
   {emph = instr.emph;
    instr = interp_bare_proof_instr info sigma env instr.instr}
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index b7c517456..4fc5862c1 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1140,10 +1140,10 @@ let case_tac params pat_info hyps gls0 =
 
 (* end cases *)
 
-type instance_stack =
-    (constr option*(constr list) list) list
+type ('a, 'b) instance_stack =
+    ('b * (('a option * constr list) list)) list
 
-let initial_instance_stack ids =
+let initial_instance_stack ids : (_, _) instance_stack =
   List.map (fun id -> id,[None,[]]) ids
 
 let push_one_arg arg = function
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 82a6c3933..ab0e480f9 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -72,7 +72,7 @@ type flag = info * scheme
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
-let rec flag_of_type env t =
+let rec flag_of_type env t : flag =
   let t = whd_betadeltaiota env none t in
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
@@ -844,7 +844,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_lams_eta_n n m env c t =
+let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
   let rels = List.map (fun (id,_,c) -> (id,c)) rels in
   let rels',c = decompose_lam c in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 321af2946..a8c9375b1 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -800,7 +800,7 @@ let rec merge_ids ids ids' = match ids,ids' with
 
 let is_exn = function MLexn _ -> true | _ -> false
 
-let rec permut_case_fun br acc =
+let permut_case_fun br acc =
   let nb = ref max_int in
   Array.iter (fun (_,_,t) ->
 		let ids, c = collect_lams t in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 3d21fc2d8..067c41705 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -120,7 +120,7 @@ let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type par vl t =
+let pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 1fd4840fe..2dd07b2f2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -67,7 +67,7 @@ let is_toplevel mp =
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
-let rec mp_length mp =
+let mp_length mp =
   let mp0 = current_toplevel () in
   let rec len = function
     | mp when mp = mp0 -> 1
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 8680b5756..5cc7f61d9 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -77,7 +77,7 @@ type kind_of_formula=
   | Forall of constr*constr
   | Atom of constr
 
-let rec kind_of_formula gl term =
+let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
     match match_with_imp_term cciterm with
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index c6ec43e7a..7e6f65eaa 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -124,7 +124,7 @@ let lookup item seq=
 	    | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
 	  History.exists p seq.history
 
-let rec add_formula side nam t seq gl=
+let add_formula side nam t seq gl=
   match build_formula side nam t gl seq.cnt with
       Left f->
 	begin
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 043c9e517..b940dee3a 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 997a18d73..b45932e57 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])
 ;;
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 567bdcd6e..cb41de283 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -423,7 +423,7 @@ let generate_functional_principle
 exception Not_Rec
 
 let get_funs_constant mp dp =
-  let rec get_funs_constant const e : (Names.constant*int) array =
+  let get_funs_constant const e : (Names.constant*int) array =
     match kind_of_term ((strip_lam e)) with
       | Fix((_,(na,_,_))) ->
 	  Array.mapi
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5b9bf44c3..0ad8bc5e6 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -188,7 +188,7 @@ let build_newrecursive l =
   build_newrecursive l'
 
 (* Checks whether or not the mutual bloc is recursive *)
-let rec is_rec names =
+let is_rec names =
   let names = List.fold_right Idset.add names Idset.empty in
   let check_id id names =  Idset.mem id names in
   let rec lookup names = function
@@ -562,7 +562,7 @@ let decompose_prod_n_assum_constr_expr =
 open Constrexpr
 open Topconstr
 
-let rec make_assoc = List.fold_left2 (fun l a b ->
+let make_assoc = List.fold_left2 (fun l a b ->
 match a, b with
   |(_,Name na), (_, Name id) -> (na, id)::l
   |_,_ -> l
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 6fff88fd8..b848d77a7 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -570,7 +570,7 @@ let rec merge_rec_hyps shift accrec
     | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
 
 
-let rec build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift =
+let build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift =
   List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
 
 
@@ -761,7 +761,7 @@ let merge_constructor_id id1 id2 shift:identifier =
 (** [merge_constructors lnk shift avoid] merges the two list of
     constructor [(name*type)]. These are translated to glob_constr
     first, each of them having distinct var names. *)
-let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
+let merge_constructors (shift:merge_infos) (avoid:Idset.t)
     (typcstr1:(identifier * glob_constr) list)
     (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list =
   List.flatten
@@ -779,7 +779,7 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
 (** [merge_inductive_body lnk shift avoid oib1 oib2] merges two
     inductive bodies [oib1] and [oib2], linking with [lnk], params
     info in [shift], avoiding identifiers in [avoid]. *)
-let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
+let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
     (oib2:one_inductive_body) =
   (* building glob_constr type of constructors *)
   let mkrawcor nme avoid typ =
@@ -813,7 +813,7 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
     [lnk]. [shift] information on parameters of the new inductive.
     For the moment, inductives are supposed to be non mutual.
 *)
-let rec merge_mutual_inductive_body
+let merge_mutual_inductive_body
     (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) =
   (* Mutual not treated, we take first ind body of each. *)
   merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 25579a878..e40a8a273 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -816,7 +816,7 @@ let pivot v (c1,p1) (c2,p2) =
 	    
 exception FoundProof of  prf_rule
 
-let rec simpl_sys sys = 
+let simpl_sys sys = 
   List.fold_left (fun acc (c,p) -> 
 		    match check_sat (c,p) with
 		    | Tauto -> acc
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 2ce7b7240..beb7b4819 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -574,7 +574,7 @@ struct
 
   let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
 
-  let rec dump_n x =
+  let dump_n x =
    match x with
     | Mc.N0 -> Lazy.force coq_N0
     | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
@@ -587,12 +587,12 @@ struct
 
   let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x)
 
-  let rec pp_n o x =  output_string o  (string_of_int (CoqToCaml.n x))
+  let pp_n o x =  output_string o  (string_of_int (CoqToCaml.n x))
 
   let dump_pair t1 t2 dump_t1 dump_t2 (x,y) =
    Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|])
 
-  let rec parse_z term =
+  let parse_z term =
    let (i,c) = get_left_construct term in
     match i with
      | 1 -> Mc.Z0
@@ -777,7 +777,7 @@ struct
         Printf.fprintf o "0" in
     pp_cone o e
 
-  let rec dump_op = function
+  let dump_op = function
    | Mc.OpEq-> Lazy.force coq_OpEq
    | Mc.OpNEq-> Lazy.force coq_OpNEq
    | Mc.OpLe -> Lazy.force coq_OpLe
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 564126d24..0537cdbe8 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1499,7 +1499,7 @@ module N =
   
   (** val eqb : n -> n -> bool **)
   
-  let rec eqb n0 m =
+  let eqb n0 m =
     match n0 with
     | N0 ->
       (match m with
@@ -1693,7 +1693,7 @@ module N =
   
   (** val ldiff : n -> n -> n **)
   
-  let rec ldiff n0 m =
+  let ldiff n0 m =
     match n0 with
     | N0 -> N0
     | Npos p ->
@@ -2205,7 +2205,7 @@ module Z =
   
   (** val eqb : z -> z -> bool **)
   
-  let rec eqb x y =
+  let eqb x y =
     match x with
     | Z0 ->
       (match y with
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ccbf0406e..240c29e0f 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -89,7 +89,7 @@ let list_try_find f =
   in
   try_find_f
 
-let rec list_fold_right_elements f l =
+let list_fold_right_elements f l =
   let rec aux = function
     | [] -> invalid_arg "list_fold_right_elements"
     | [x] -> x
@@ -142,7 +142,7 @@ let rec rec_gcd_list c l  =
   | [] -> c
   | e::l -> rec_gcd_list (gcd_big_int  c (numerator e)) l
 
-let rec gcd_list l =
+let gcd_list l =
  let res = rec_gcd_list zero_big_int l in
   if compare_big_int res zero_big_int = 0
   then unit_big_int else res
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 36b05a725..1f7c083e2 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -315,7 +315,7 @@ module Vect =
 	if Big_int.compare_big_int res Big_int.zero_big_int = 0
 	then Big_int.unit_big_int else res
 
-    let rec mul z t =
+    let mul z t =
       match z with
 	| Int 0 -> []
 	| Int 1 -> t
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index d5efb5cef..e0b27a2f5 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -764,7 +764,7 @@ let slice i a q =
 
 (* sugar strategy *)
 
-let rec addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat deconne *)
+let addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat deconne *)
 			  
 let addSsugar x l =
   if !sugar_flag
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 97db0f731..4cac90713 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -420,7 +420,7 @@ let pol_sparse_to_term n2 p =
   aux p
 
 
-let rec remove_list_tail l i =
+let remove_list_tail l i =
   let rec aux l i =
     if l=[]
     then []
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index e030c2822..071df5cf7 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -160,7 +160,7 @@ let rec max_var_pol2 p =
       Pint _ -> 0
     |Prec(v,c)-> Array.fold_right (fun q m -> max (max_var_pol2 q) m) c v
 
-let rec max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
+let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
 
 (* equality between polynomials *)
 
@@ -181,7 +181,7 @@ let rec equal p q =
    if constant, returns the coefficient
 *)
 
-let rec norm p = match p with
+let norm p = match p with
     Pint _ -> p
   |Prec (x,a)->
      let d = (Array.length a -1) in
@@ -198,7 +198,7 @@ let rec norm p = match p with
 
 
 (* degree in v, v >= max var of p *)
-let rec deg v p =
+let deg v p =
   match p with
       Prec(x,p1) when x=v -> Array.length p1 -1
     |_ -> 0
@@ -276,7 +276,7 @@ let rec vars=function
 
 
 (* multiply p by v^n, v >= max_var p *)
-let rec multx n v p =
+let multx n v p =
   match p with
       Prec (x,p1) when x=v -> let p2= Array.create ((Array.length p1)+n) (Pint coef0) in
         for i=0 to (Array.length p1)-1 do
@@ -314,7 +314,7 @@ let rec multP p q =
 
 
 (* derive p with variable v, v >= max_var p *)
-let rec deriv v p =
+let deriv v p =
   match p with
       Pint a -> Pint coef0
     | Prec(x,p1) when x=v ->
@@ -656,7 +656,7 @@ and gcd_sub_res_rec p q s c d x =
 
 and lazard_power c s d x =
   let res = ref c in
-    for i=1 to d-1 do
+    for _i = 1 to d - 1 do
       res:= div_pol ((!res)@@c) s x;
     done;
     !res
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 ->
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 931ce400e..50031052b 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -302,7 +302,7 @@ let omega_of_oformula env kind =
 
 (* \subsection{Omega vers Oformula} *)
 
-let rec oformula_of_omega env af =
+let oformula_of_omega env af =
   let rec loop = function
     | ({v=v; c=n}::r) ->
 	Oplus(Omult(unintern_omega env v,Oint n),loop r)
@@ -313,7 +313,7 @@ let app f v = mkApp(Lazy.force f,v)
 
 (* \subsection{Oformula vers COQ reel} *)
 
-let rec coq_of_formula env t =
+let coq_of_formula env t =
   let rec loop = function
   | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |]
   | Oopp t -> app Z.opp [| loop t |]
@@ -477,11 +477,11 @@ let rec negate = function
  | Oufo c -> do_list [], Oufo (Oopp c)
  | Ominus _ -> failwith "negate minus"
 
-let rec norm l = (List.length l)
+let norm l = (List.length l)
 
 (* \subsection{Mélange (fusion) de deux équations} *)
 (* \subsubsection{Version avec coefficients} *)
-let rec shuffle_path k1 e1 k2 e2 =
+let shuffle_path k1 e1 k2 e2 =
   let rec loop = function
       (({c=c1;v=v1}::l1) as l1'),
       (({c=c2;v=v2}::l2) as l2') ->
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 17dd563f7..88cc07c0e 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -63,7 +63,7 @@ let uninterp_ascii r =
     | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
-    let rec aux = function
+    let aux = function
     | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 75bc84074..c03b13b5a 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -210,7 +210,7 @@ let param_attribute_of_params params =
 ;;
 
 let print_object uri ids_to_inner_sorts =
- let rec aux =
+ let aux =
   let module A = Acic in
   let module X = Xml in
     function
diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4
index 8a4eb39a1..c2523755b 100644
--- a/plugins/xml/xml.ml4
+++ b/plugins/xml/xml.ml4
@@ -55,7 +55,7 @@ let pp_ch strm channel =
       pp_r m s
   | [< >] -> ()
  and print_spaces m =
-  for i = 1 to m do fprint_string "  " done
+  for _i = 1 to m do fprint_string "  " done
  and fprint_string str =
   output_string channel str
  in