diff options
Diffstat (limited to 'plugins')
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 |