diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-18 15:42:36 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-18 15:42:36 +0000 |
| commit | ddc9c1bd8e1eaae186468f093e467d8f2e1091cd (patch) | |
| tree | 6543bbcdca657cfd315be224531f66fed5adb280 /plugins/xml/cic2acic.ml | |
| parent | 648c594489f8d0ffdde9596b87f5c1ff6ccef612 (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 'plugins/xml/cic2acic.ml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |