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/cic2acic.ml | 2 +- plugins/xml/xmlcommand.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 2772779d4..90712c473 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -457,7 +457,7 @@ print_endline "PASSATO" ; flush stdout ; let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in let he1'' = String.concat "/" - (List.map Names.Id.to_string (List.rev he1')) ^ "/" + (List.rev_map Names.Id.to_string he1') ^ "/" ^ (Names.Id.to_string he1_id) ^ ".var" in (he1'',he2)::subst, extra_args, uninst diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 479b04228..91e15e8a6 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