From 18ebb3f525a965358d96eab7df493450009517b5 Mon Sep 17 00:00:00 2001 From: regisgia Date: Fri, 14 Sep 2012 09:52:38 +0000 Subject: 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 --- plugins/extraction/extraction.ml | 4 ++-- plugins/extraction/mlutil.ml | 2 +- plugins/extraction/ocaml.ml | 2 +- plugins/extraction/table.ml | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/extraction') 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 -- cgit v1.2.3