aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorletouzey2013-02-18 15:42:36 +0000
committerletouzey2013-02-18 15:42:36 +0000
commitddc9c1bd8e1eaae186468f093e467d8f2e1091cd (patch)
tree6543bbcdca657cfd315be224531f66fed5adb280 /tools
parent648c594489f8d0ffdde9596b87f5c1ff6ccef612 (diff)
use List.rev_map whenever possible
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep_common.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 4977a94cd7..235aa30745 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -141,7 +141,7 @@ let warning_clash file dir =
let f = Filename.basename f1 in
let d1 = Filename.dirname f1 in
let d2 = Filename.dirname f2 in
- let dl = List.map Filename.dirname (List.rev fl) in
+ let dl = List.rev_map Filename.dirname fl in
eprintf
"*** Warning: in file %s, \n required library %s matches several files in path\n (found %s.v in "
file (String.concat "." dir) f;