aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/xmlcommand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
-rw-r--r--plugins/xml/xmlcommand.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 35760a51d..50309317e 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -46,7 +46,7 @@ let filter_params pvars hyps =
let cwd = Lib.cwd () in
let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
- aux (Names.repr_dirpath modulepath) (List.rev pvars)
+ aux (Names.Dir_path.repr modulepath) (List.rev pvars)
;;
(* The computation is very inefficient, but we can't do anything *)
@@ -62,7 +62,7 @@ let search_variables () =
[] -> []
| he::tl as modules ->
let one_section_variables =
- let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
+ let dirpath = N.Dir_path.make (modules @ N.Dir_path.repr modulepath) in
let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in
[he,t]
in
@@ -113,7 +113,7 @@ let theory_filename xml_library_root =
match xml_library_root with
None -> None (* stdout *)
| Some xml_library_root' ->
- let toks = List.map N.Id.to_string (N.repr_dirpath (Lib.library_dp ())) in
+ let toks = List.map N.Id.to_string (N.Dir_path.repr (Lib.library_dp ())) in
(* theory from A/B/C/F.v goes into A/B/C/F.theory *)
let alltoks = List.rev toks in
Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -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.repr_dirpath dir)))
+ (List.map Names.Id.to_string (List.rev (Names.Dir_path.repr dir)))
;;
let _ =
@@ -550,5 +550,5 @@ let _ =
Library.set_xml_require
(fun d -> theory_output_string
(Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
- (uri_of_dirpath d) (Names.string_of_dirpath d)))
+ (uri_of_dirpath d) (Names.Dir_path.to_string d)))
;;