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 /library | |
| 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
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | library/nametab.ml | 8 |
3 files changed, 5 insertions, 7 deletions
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, |