aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml')
-rw-r--r--plugins/xml/cic2acic.ml2
-rw-r--r--plugins/xml/xmlcommand.ml4
2 files changed, 3 insertions, 3 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
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 _ =