From ddc9c1bd8e1eaae186468f093e467d8f2e1091cd Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 18 Feb 2013 15:42:36 +0000
Subject: use List.rev_map whenever possible

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/include')

diff --git a/checker/include b/checker/include
index b7d46d4b3..0b68da4b7 100644
--- a/checker/include
+++ b/checker/include
@@ -127,7 +127,7 @@ let mod_access m fld =
 ;;
 
 let parse_dp s =
-  make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s)))
+  make_dirpath(List.rev_map id_of_string (Str.split(Str.regexp"\\.") s))
 ;;
 let parse_sp s =
   let l = List.rev (Str.split(Str.regexp"\\.") s) in
-- 
cgit v1.2.3