diff options
81 files changed, 167 insertions, 172 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 1a2bf3c34..e65e41847 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -289,7 +289,7 @@ let print_pure_constr csr = print_string "Fix("; print_int i; print_string ")"; print_cut(); open_vbox 0; - let rec print_fix () = + let print_fix () = for k = 0 to (Array.length tl) - 1 do open_vbox 0; name_display lna.(k); print_string "/"; @@ -303,7 +303,7 @@ let print_pure_constr csr = print_string "CoFix("; print_int i; print_string ")"; print_cut(); open_vbox 0; - let rec print_fix () = + let print_fix () = for k = 0 to (Array.length tl) - 1 do open_vbox 1; name_display lna.(k); print_cut(); print_string ":"; diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index bf67735dc..3fd460058 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -208,7 +208,7 @@ let rec mlexpr_of_argtype loc = function <:expr< Genarg.PairArgType $t1$ $t2$ >> | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> -let rec mlexpr_of_may_eval f = function +let mlexpr_of_may_eval f = function | Genredexpr.ConstrEval (r,c) -> <:expr< Genredexpr.ConstrEval $mlexpr_of_red_expr r$ $f c$ >> | Genredexpr.ConstrContext ((loc,id),c) -> diff --git a/interp/notation.ml b/interp/notation.ml index 630f64f7b..6a574a56e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -392,7 +392,7 @@ let interp_prim_token = let interp_prim_token_cases_pattern_expr loc looked_for p = interp_prim_token_gen (Constrexpr_ops.raw_cases_pattern_expr_of_glob_constr looked_for) loc p -let rec interp_notation loc ntn local_scopes = +let interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in try find_interpretation ntn (find_notation ntn) scopes with Not_found -> diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ad1bd1138..ae851d8ba 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -110,7 +110,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function | NPatVar n -> GPatVar (loc,(false,n)) | NRef x -> GRef (loc,x) -let rec glob_constr_of_notation_constr loc x = +let glob_constr_of_notation_constr loc x = let rec aux () x = glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x @@ -544,7 +544,7 @@ let rec match_iterated_binders islambda decls = function let remove_sigma x (sigmavar,sigmalist,sigmabinders) = (List.remove_assoc x sigmavar,sigmalist,sigmabinders) -let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin = +let match_abinderlist_with_app match_fun metas sigma rest x iter termin = let rec aux sigma acc rest = try let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index d6b3a9596..7a40a4029 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -220,7 +220,7 @@ let pos_rel i r sz = (* non-terminating instruction (branch, raise, return, appterm) *) (* in front of it. *) -let rec discard_dead_code cont = cont +let discard_dead_code cont = cont (*function [] -> [] | (Klabel _ | Krestart ) :: _ as cont -> cont diff --git a/kernel/environ.ml b/kernel/environ.ml index 2c723a834..f1adb5340 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -317,7 +317,7 @@ let compile_constant_body = Cbytegen.compile_constant_body exception Hyp_not_found -let rec apply_to_hyp (ctxt,vals) id f = +let apply_to_hyp (ctxt,vals) id f = let rec aux rtail ctxt vals = match ctxt, vals with | (idc,c,ct as d)::ctxt, v::vals -> @@ -330,7 +330,7 @@ let rec apply_to_hyp (ctxt,vals) id f = | _, _ -> assert false in aux [] ctxt vals -let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g = +let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = let rec aux ctxt vals = match ctxt,vals with | (idc,c,ct as d)::ctxt, v::vals -> diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 7c0b14dce..a9d4d8832 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -147,7 +147,7 @@ let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver let mp_of_delta resolve mp = try Deltamap.find_mp mp resolve with Not_found -> mp -let rec find_prefix resolve mp = +let find_prefix resolve mp = let rec sub_mp = function | MPdot(mp,l) as mp_sup -> (try Deltamap.find_mp mp_sup resolve diff --git a/kernel/term.ml b/kernel/term.ml index 9a25de1bc..16649b181 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -108,6 +108,8 @@ type ('constr, 'types) kind_of_term = -rectypes of the Caml compiler to be set *) type constr = (constr,constr) kind_of_term +type strategy = types option + type existential = existential_key * constr array type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration @@ -429,7 +431,7 @@ let rec under_casts f c = match kind_of_term c with (******************************************************************) (* flattens application lists throwing casts in-between *) -let rec collapse_appl c = match kind_of_term c with +let collapse_appl c = match kind_of_term c with | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term (strip_outer_cast f) with @@ -647,8 +649,6 @@ let rec constr_ord m n= type types = constr -type strategy = types option - type named_declaration = identifier * constr option * types type rel_declaration = name * constr option * types diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9487b6d39..608bcc886 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -95,7 +95,7 @@ let judge_of_variable env id = (* Checks if a context of variable can be instantiated by the variables of the current env *) (* TODO: check order? *) -let rec check_hyps_inclusion env sign = +let check_hyps_inclusion env sign = Sign.fold_named_context (fun (id,_,ty1) () -> let ty2 = named_type id env in diff --git a/lib/bigint.ml b/lib/bigint.ml index d307de4d9..9012d9322 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -100,7 +100,7 @@ let normalize_neg n = input: an array with first bloc in [-base;base[ and others in [0;base[ output: a canonical array *) -let rec normalize n = +let normalize n = if Array.length n = 0 then n else if n.(0) = -1 then normalize_neg n else if n.(0) = 0 then normalize_pos n @@ -172,7 +172,7 @@ let sub n m = if d >= 0 then sub_to (Array.copy n) m d else let r = neg m in add_to r n (Array.length r - Array.length n) -let rec mult m n = +let mult m n = if m = zero or n = zero then zero else let l = Array.length m + Array.length n in let r = Array.create l 0 in diff --git a/lib/dnet.ml b/lib/dnet.ml index 0562cc40b..a9e1e97e3 100644 --- a/lib/dnet.ml +++ b/lib/dnet.ml @@ -169,13 +169,13 @@ struct (* Sets with a neutral element for inter *) module OSet (S:Set.S) = struct type t = S.t option - let union s1 s2 = match s1,s2 with + let union s1 s2 : t = match s1,s2 with | (None, _ | _, None) -> None | Some a, Some b -> Some (S.union a b) - let inter s1 s2 = match s1,s2 with + let inter s1 s2 : t = match s1,s2 with | (None, a | a, None) -> a | Some a, Some b -> Some (S.inter a b) - let is_empty = function + let is_empty : t -> bool = function | None -> false | Some s -> S.is_empty s (* optimization hack: Not_found is catched in fold_pattern *) diff --git a/lib/explore.ml b/lib/explore.ml index 1c8776a4a..90258b0e5 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -21,7 +21,7 @@ module Make = functor(S : SearchProblem) -> struct type position = int list - let msg_with_position p pp = + let msg_with_position (p : position) pp = let rec pp_rec = function | [] -> mt () | [i] -> int i @@ -58,7 +58,7 @@ module Make = functor(S : SearchProblem) -> struct let empty = [],[] - let push x (h,t) = (x::h,t) + let push x (h,t) : _ queue = (x::h,t) let pop = function | h, x::t -> x, (h,t) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 5f4738dcf..7c2897be0 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -60,7 +60,6 @@ module Make(X:Comp) = *) module Htbl = Hashtbl.Make( struct type t=X.t - type u=X.u let hash=X.hash let equal x1 x2 = (*incr comparaison;*) X.equal x1 x2 end) @@ -71,8 +71,6 @@ type ppcmd = (int*string) ppcmd_token type std_ppcmds = ppcmd Stream.t -type 'a ppdirs = 'a ppdir_token Stream.t - let is_empty s = try Stream.empty s; true with Stream.Failure -> false @@ -175,7 +173,7 @@ let rec eval_ppcmds l = Stream.of_list (aux l) (* In new syntax only double quote char is escaped by repeating it *) -let rec escape_string s = +let escape_string s = let rec escape_at s i = if i<0 then s else if s.[i] == '"' then diff --git a/lib/profile.ml b/lib/profile.ml index 2472d75df..9002972d9 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -221,7 +221,7 @@ let loops = 10000 let time_overhead_A_D () = let e = create_record () in let before = get_time () in - for i=1 to loops do + for _i = 1 to loops do (* This is a copy of profile1 for overhead estimation *) let dw = dummy_spent_alloc () in match !dummy_stack with [] -> assert false | p::_ -> @@ -245,7 +245,7 @@ let time_overhead_A_D () = done; let after = get_time () in let beforeloop = get_time () in - for i=1 to loops do () done; + for _i = 1 to loops do () done; let afterloop = get_time () in float_of_int ((after - before) - (afterloop - beforeloop)) /. float_of_int loops @@ -253,7 +253,7 @@ let time_overhead_A_D () = let time_overhead_B_C () = let dummy_x = 0 in let before = get_time () in - for i=1 to loops do + for _i = 1 to loops do try dummy_last_alloc := get_alloc (); let _r = dummy_f dummy_x in @@ -264,7 +264,7 @@ let time_overhead_B_C () = done; let after = get_time () in let beforeloop = get_time () in - for i=1 to loops do () done; + for _i = 1 to loops do () done; let afterloop = get_time () in float_of_int ((after - before) - (afterloop - beforeloop)) /. float_of_int loops diff --git a/lib/rtree.ml b/lib/rtree.ml index 8f859b47e..b7fe9184e 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -101,7 +101,7 @@ let rec map f t = match t with | Node (a,sons) -> Node (f a, Array.map (map f) sons) | Rec(j,defs) -> Rec (j, Array.map (map f) defs) -let rec smartmap f t = match t with +let smartmap f t = match t with Param _ -> t | Node (a,sons) -> let a'=f a and sons' = Util.array_smartmap (map f) sons in diff --git a/lib/serialize.ml b/lib/serialize.ml index 0f19badf4..04405ac1b 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -508,7 +508,7 @@ let pr_option_value = function | StringValue s -> s | BoolValue b -> if b then "true" else "false" -let rec pr_setoptions opts = +let pr_setoptions opts = let map (key, v) = let key = String.concat " " key in key ^ " := " ^ (pr_option_value v) diff --git a/lib/system.ml b/lib/system.ml index bfa46c4b3..e721b1f65 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -58,7 +58,7 @@ let where_in_path ?(warn=true) path filename = then (lpe,f) :: search rem else search rem | [] -> [] in - let rec check_and_warn l = + let check_and_warn l = match l with | [] -> raise Not_found | (lpe, f) :: l' -> diff --git a/lib/util.ml b/lib/util.ml index ddc88e83b..1365f53ce 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -548,7 +548,7 @@ let rec list_fold_left3 f accu l1 l2 l3 = a1 []] *) -let rec list_fold_right_and_left f l hd = +let list_fold_right_and_left f l hd = let rec aux tl = function | [] -> hd | a::l -> let hd = aux (a::tl) l in f hd a tl @@ -636,7 +636,7 @@ let list_uniquize l = | [] -> List.rev acc in aux [] l -let rec list_distinct l = +let list_distinct l = let visited = Hashtbl.create 23 in let rec loop = function | h::t -> @@ -774,7 +774,7 @@ let rec list_skipn n l = match n,l with | _, [] -> failwith "list_skipn" | n, _::l -> list_skipn (pred n) l -let rec list_skipn_at_least n l = +let list_skipn_at_least n l = try list_skipn n l with Failure _ -> [] let list_prefix_of prefl l = @@ -852,7 +852,7 @@ let list_union_map f l acc = [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], and so on if there are more elements in the lists. *) -let rec list_cartesian op l1 l2 = +let list_cartesian op l1 l2 = list_map_append (fun x -> List.map (op x) l2) l1 (* [list_cartesians] is an n-ary cartesian product: it iterates @@ -874,12 +874,12 @@ let rec list_combine3 x y z = (* Keep only those products that do not return None *) -let rec list_cartesian_filter op l1 l2 = +let list_cartesian_filter op l1 l2 = list_map_append (fun x -> list_map_filter (op x) l2) l1 (* Keep only those products that do not return None *) -let rec list_cartesians_filter op init ll = +let list_cartesians_filter op init ll = List.fold_right (list_cartesian_filter op) ll [init] (* Drop the last element of a list *) @@ -1217,15 +1217,6 @@ let array_filter_along f filter v = let array_filter_with filter v = Array.of_list (list_filter_with filter (Array.to_list v)) -(* Stream *) - -let stream_nth n st = - try List.nth (Stream.npeek (n+1) st) n - with Failure _ -> raise Stream.Failure - -let stream_njunk n st = - for i = 1 to n do Stream.junk st done - (* Matrices *) let matrix_transpose mat = @@ -1247,7 +1238,7 @@ let iterate f = iterate_f let repeat n f x = - for i = 1 to n do f x done + let rec loop i = if i <> 0 then (f x; loop (i - 1)) in loop n let iterate_for a b f x = let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in @@ -1258,6 +1249,15 @@ let app_opt f x = | Some f -> f x | None -> x +(* Stream *) + +let stream_nth n st = + try List.nth (Stream.npeek (n+1) st) n + with Failure _ -> raise Stream.Failure + +let stream_njunk n st = + repeat n Stream.junk st + (* Delayed computations *) type 'a delayed = unit -> 'a diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml index 48ee546ca..0a3b5da47 100644 --- a/lib/xml_utils.ml +++ b/lib/xml_utils.ml @@ -116,7 +116,7 @@ let buffer_attr (n,v) = done; Buffer.add_char tmp '"' -let rec print_attr chan (n, v) = +let print_attr chan (n, v) = Printf.fprintf chan " %s=\"" n; let l = String.length v in for p = 0 to l-1 do diff --git a/library/declaremods.ml b/library/declaremods.ml index 4d8a65651..a61e59d6d 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1043,7 +1043,7 @@ let iter_all_segments f = List.iter apply_obj objects) !modtab_objects in - let rec apply_node = function + let apply_node = function | sp, Leaf o -> f sp o | _ -> () in diff --git a/library/impargs.ml b/library/impargs.ml index 30a402302..a7d4bcbfb 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -695,7 +695,7 @@ let rec select_impargs_size n = function | (LessArgsThan p, impls)::l -> if n <= p then impls else select_impargs_size n l -let rec select_stronger_impargs = function +let select_stronger_impargs = function | [] -> [] (* Tolerance for (DefaultImpArgs,[]) *) | (_,impls)::_ -> impls diff --git a/library/nametab.ml b/library/nametab.ml index cae6e7278..0aac3873a 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -505,8 +505,8 @@ let global_inductive r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * kntab * kntab - * globrevtab * mprevtab * knrevtab * knrevtab +type frozen = ccitab * dirtab * mptab * kntab + * globrevtab * mprevtab * mptrevtab * knrevtab let init () = the_ccitab := SpTab.empty; @@ -518,9 +518,7 @@ let init () = the_modtyperevtab := MPmap.empty; the_tacticrevtab := KNmap.empty - - -let freeze () = +let freeze () : frozen = !the_ccitab, !the_dirtab, !the_modtypetab, diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index d95dea22c..14644339c 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -389,10 +389,10 @@ let rec progress_further last nj tt cs = and update_longest_valid_token last nj tt cs = match tt.node with | Some _ as last' -> - for i=1 to nj do Stream.junk cs done; - progress_further last' 0 tt cs + stream_njunk nj cs; + progress_further last' 0 tt cs | None -> - progress_further last nj tt cs + progress_further last nj tt cs (* nj is the number of char peeked since last valid token *) (* n the number of char in utf8 block *) 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 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 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8cfc3f9d9..c077fbe83 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -639,7 +639,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function | ExtraRedExpr s -> str s | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o -let rec pr_may_eval test prc prlc pr2 pr3 = function +let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> hov 0 (str "eval" ++ brk (1,1) ++ diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 23b98d415..50baf36f8 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -122,7 +122,7 @@ let pr_with_constr prc = function | None -> mt () | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) -let rec pr_message_token prid = function +let pr_message_token prid = function | MsgString s -> qs s | MsgInt n -> int n | MsgIdent id -> prid id diff --git a/proofs/logic.ml b/proofs/logic.ml index ff4f19aad..a79485d1e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -147,7 +147,7 @@ let push_val y = function let push_item x v (m,l) = (Idmap.add x v m, (x,Idset.empty)::l) let mem_q x (m,_) = Idmap.mem x m -let rec find_q x (m,q) = +let find_q x (m,q) = let v = Idmap.find x m in let m' = Idmap.remove x m in let rec find accs acc = function diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 6ffc79246..a3e240c8d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -100,7 +100,7 @@ let _ = Errors.register_handler begin function | NoSuchProof -> Errors.error "No such proof." | _ -> raise Errors.Unhandled end -let rec extract id l = +let extract id l = let rec aux = function | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l) | np::l -> let (np', l) = aux l in (np' , np::l) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index dbb295969..0e2ac1dde 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -372,7 +372,7 @@ let list_of_sensitive s k env = with e when catchable_exception e -> tclZERO e env -let rec tclGOALBIND s k = +let tclGOALBIND s k = (* spiwack: the first line ensures that the value returned by the tactic [k] will not "escape its scope". *) let k a = tclBIND (k a) here_s in @@ -380,7 +380,7 @@ let rec tclGOALBIND s k = tclDISPATCHGEN Goal.null Goal.plus tacs end -let rec tclGOALBINDU s k = +let tclGOALBINDU s k = tclBIND (list_of_sensitive s k) begin fun tacs -> tclDISPATCHGEN () unitK tacs end diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 39f1bf287..49026cc0b 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -104,7 +104,7 @@ let run_com inst = let run ini = if not ini then begin - for i=1 to 2 do + for _i = 1 to 2 do print_char (Char.chr 8);print_char (Char.chr 13) done; msg_tac_debug (str "Executed expressions: " ++ int !skipped ++ fnl()) 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 diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 4a5634673..7e400a332 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -692,7 +692,7 @@ let warn_install_at_root_directory let check_overlapping_include (_,inc_r) = let pwd = Sys.getcwd () in - let rec aux = function + let aux = function | [] -> () | (pdir,_,abspdir)::l -> if not (is_prefix pwd abspdir) then diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4 index 1a9b9c73f..42d3f8f0a 100644 --- a/tools/coq_tex.ml4 +++ b/tools/coq_tex.ml4 @@ -122,7 +122,7 @@ let insert texfile coq_output result = let next_block k = if !last_read = "" then last_read := input_line c_coq; (* skip k prompts *) - for i = 1 to k do + for _i = 1 to k do last_read := remove_prompt !last_read; done; (* read and return the following lines until a prompt is found *) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 45f8e34b1..a8c108f4e 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -20,7 +20,7 @@ let option_D = ref false let option_w = ref false let option_sort = ref false -let rec warning_mult suf iter = +let warning_mult suf iter = let tab = Hashtbl.create 151 in let check f d = begin try diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index dc38d3bce..86a5b0cbe 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -566,7 +566,7 @@ module Html = struct printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true) end - let indentation n = for i = 1 to n do printf " " done + let indentation n = for _i = 1 to n do printf " " done let line_break () = printf "<br/>\n" @@ -1128,7 +1128,7 @@ module Raw = struct let stop_quote () = printf "\"" let indentation n = - for i = 1 to n do printf " " done + for _i = 1 to n do printf " " done let keyword s loc = raw_ident s let ident s loc = raw_ident s diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 14fe2855b..e8abd8e17 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -47,7 +47,7 @@ and aux = function if n > (List.length l) then failwith "quick_chop args" else kick_last (aux (n,l) ) -let rec deconstruct_type t = +let deconstruct_type t = let l,r = decompose_prod t in (List.map (fun (_,b) -> b) (List.rev l))@[r] diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 912d694eb..2d919e966 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -62,7 +62,7 @@ let npop n = (* Since our history stack always contains an initial entry, it's invalid to try to completely empty it *) if n < 0 || n >= Stack.length history then raise Invalid - else for i = 1 to n do pop () done + else for _i = 1 to n do pop () done let top () = try Stack.top history with Stack.Empty -> raise Invalid @@ -107,7 +107,7 @@ let mark_command ast = [pnum] and finally going to state number [snum]. *) let raw_backtrack snum pnum naborts = - for i = 1 to naborts do Pfedit.delete_current_proof () done; + for _i = 1 to naborts do Pfedit.delete_current_proof () done; Pfedit.undo_todepth pnum; Lib.reset_label snum diff --git a/toplevel/command.ml b/toplevel/command.ml index e45005ac3..3ccfe21d8 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -895,7 +895,7 @@ let do_program_recursive fixkind fixl ntns = let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in (* Solve remaining evars *) let evd = nf_evar_map_undefined evd in - let rec collect_evars id def typ imps = + let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index e80ff8b61..bb60fed73 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -353,7 +353,7 @@ let do_mutual_induction_scheme lnamedepindsort = lnamedepindsort in let listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in - let rec declare decl fi lrecref = + let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 Evd.empty decl in let decltype = refresh_universes decltype in let cst = define fi UserVerbose decl (Some decltype) in diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 2e7b37db7..77949a126 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -429,7 +429,7 @@ let is_prod_ident = function | Terminal s when is_letter s.[0] or s.[0] = '_' -> true | _ -> false -let rec is_non_terminal = function +let is_non_terminal = function | NonTerminal _ | SProdList _ -> true | _ -> false |