From ddc9c1bd8e1eaae186468f093e467d8f2e1091cd Mon Sep 17 00:00:00 2001
From: letouzey
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
---
 plugins/xml/xmlcommand.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/xml/xmlcommand.ml')

diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 479b04228e..91e15e8a6f 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -35,7 +35,7 @@ let filter_params pvars hyps =
       let ids' = id::ids in
       let ids'' =
        "cic:/" ^
-        String.concat "/" (List.rev (List.map Names.Id.to_string ids')) in
+        String.concat "/" (List.rev_map Names.Id.to_string ids') in
       let he' =
        ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in
       let tl' = aux ids' tl in
@@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
-    (List.map Names.Id.to_string (List.rev (Names.Dir_path.repr dir)))
+    (List.rev_map Names.Id.to_string (Names.Dir_path.repr dir))
 ;;
 
 let _ =
-- 
cgit v1.2.3