From f42dd8d8530e6227621ccd662741f1da23700304 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:57:08 +0000 Subject: Modulification of dir_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/xml/cic2acic.ml | 18 +++++++++--------- plugins/xml/doubleTypeInference.ml | 2 +- plugins/xml/xmlcommand.ml | 10 +++++----- 3 files changed, 15 insertions(+), 15 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index d817396f1..fb951b35f 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -36,7 +36,7 @@ let get_module_path_of_full_path path = let remove_module_dirpath_from_dirpath ~basedir dir = let module Ln = Libnames in if Ln.is_dirpath_prefix_of basedir dir then - let ids = Names.repr_dirpath dir in + let ids = Names.Dir_path.repr dir in let rec remove_firsts n l = match n,l with (0,l) -> l @@ -46,11 +46,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir = let ids' = List.rev (remove_firsts - (List.length (Names.repr_dirpath basedir)) + (List.length (Names.Dir_path.repr basedir)) (List.rev ids)) in ids' - else Names.repr_dirpath dir + else Names.Dir_path.repr dir ;; @@ -61,7 +61,7 @@ let get_uri_of_var v pvars = function [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> - let dirpath = N.make_dirpath modules in + let dirpath = N.Dir_path.make modules in if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then modules else @@ -71,7 +71,7 @@ let get_uri_of_var v pvars = if List.mem v pvars then [] else - search_in_open_sections (N.repr_dirpath (Lib.cwd ())) + search_in_open_sections (N.Dir_path.repr (Lib.cwd ())) in "cic:" ^ List.fold_left @@ -106,21 +106,21 @@ let ext_of_tag = exception FunctorsXMLExportationNotImplementedYet;; let subtract l1 l2 = - let l1' = List.rev (Names.repr_dirpath l1) in - let l2' = List.rev (Names.repr_dirpath l2) in + let l1' = List.rev (Names.Dir_path.repr l1) in + let l2' = List.rev (Names.Dir_path.repr l2) in let rec aux = function he::tl when tl = l2' -> [he] | he::tl -> he::(aux tl) | [] -> assert (l2' = []) ; [] in - Names.make_dirpath (List.rev (aux l1')) + Names.Dir_path.make (List.rev (aux l1')) ;; let token_list_of_path dir id tag = let module N = Names in let token_list_of_dirpath dirpath = - List.rev_map N.Id.to_string (N.repr_dirpath dirpath) in + List.rev_map N.Id.to_string (N.Dir_path.repr dirpath) in token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)] let token_list_of_kernel_name tag = diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index 8f1d97d3b..b4ec85ab7 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -20,7 +20,7 @@ let cprop = N.make_con (N.MPfile (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) - (N.make_dirpath []) + (N.Dir_path.make []) (N.mk_label "CProp") ;; 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 "Require %s.
" - (uri_of_dirpath d) (Names.string_of_dirpath d))) + (uri_of_dirpath d) (Names.Dir_path.to_string d))) ;; -- cgit v1.2.3