diff options
| author |  regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 09:52:38 +0000 |
|---|---|---|
| committer | regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 09:52:38 +0000 |
| commit | 18ebb3f525a965358d96eab7df493450009517b5 (patch) | |
| tree | 8a2488055203831506010a00bb1ac0bb6fc93750 | |
| parent | 338608a73bc059670eb8196788c45a37419a3e4d (diff) | |
The new ocaml compiler (4.00) has a lot of very cool warnings,
especially about unused definitions, unused opens and unused rec
flags.
The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.
(a) "unused rec flags". They cannot change the semantics of the program
but only allow the inliner to do a better job.
(b) "unused type definitions". I only removed type definitions that were
given to functors that do not require them. Some type definitions were
used as documentation to obtain better error messages, but were not
ascribed to any definition. I superficially mentioned them in one
arbitrary chosen definition to remove the warning. This is unaesthetic
but I did not find a better way.
(c) "unused for loop index". The following idiom of imperative
programming is used at several places: "for i = 1 to n do
that_side_effect () done". I replaced "i" with "_i" to remove the
warning... but, there is a combinator named "Util.repeat" that
would only cost us a function call while improving readibility.
Should'nt we use it?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |