aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml4
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/decl_mode/decl_interp.ml4
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml6
-rw-r--r--plugins/extraction/extraction.ml4
-rw-r--r--plugins/extraction/mlutil.ml2
-rw-r--r--plugins/extraction/ocaml.ml2
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--plugins/firstorder/formula.ml2
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/fourier/fourier.ml10
-rw-r--r--plugins/fourier/fourierR.ml12
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/merge.ml8
-rw-r--r--plugins/micromega/certificate.ml2
-rw-r--r--plugins/micromega/coq_micromega.ml8
-rw-r--r--plugins/micromega/micromega.ml6
-rw-r--r--plugins/micromega/mutils.ml4
-rw-r--r--plugins/micromega/polynomial.ml2
-rw-r--r--plugins/nsatz/ideal.ml2
-rw-r--r--plugins/nsatz/nsatz.ml42
-rw-r--r--plugins/nsatz/polynom.ml12
-rw-r--r--plugins/omega/coq_omega.ml12
-rw-r--r--plugins/romega/refl_omega.ml8
-rw-r--r--plugins/syntax/ascii_syntax.ml2
-rw-r--r--plugins/xml/acic2Xml.ml42
-rw-r--r--plugins/xml/xml.ml42
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