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
---
 library/declare.ml | 2 +-
 library/library.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 27aecfe73d..3627df7fe6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -138,7 +138,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
   let args = Array.to_list (instance_from_variable_context sechyps) in
-  List.rev (List.map (Libnames.make_path dir) args)
+  List.rev_map (Libnames.make_path dir) args
 
 let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   let con = constant_of_kn kn in
diff --git a/library/library.ml b/library/library.ml
index e4e687bec6..0fdd6d75ef 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) =
 
 let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
-    (List.map Id.to_string (List.rev (Dir_path.repr dir)))
+    (List.rev_map Id.to_string (Dir_path.repr dir))
 
 let root_paths_matching_dir_path dir =
   let rec aux = function
-- 
cgit v1.2.3