Dir_path --> DirPath

 Ok, this is merely a matter of taste, but up to now the usage
 in Coq is rather to use capital letters instead of _ in the
 names of inner modules.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 15 insertions, 15 deletions

diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 90712c473..5f4add47a 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -38,7 +38,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.Dir_path.repr dir in
+   let ids = Names.DirPath.repr dir in
    let rec remove_firsts n l =
     match n,l with
        (0,l) -> l
@@ -48,11 +48,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
     let ids' =
      List.rev
       (remove_firsts
-        (List.length (Names.Dir_path.repr basedir))
+        (List.length (Names.DirPath.repr basedir))
         (List.rev ids))
     in
      ids'
-  else Names.Dir_path.repr dir
+  else Names.DirPath.repr dir
 ;;
 
 
@@ -63,7 +63,7 @@ let get_uri_of_var v pvars =
    function
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
-       let dirpath = N.Dir_path.make modules in
+       let dirpath = N.DirPath.make modules in
         if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then
          modules
         else
@@ -73,7 +73,7 @@ let get_uri_of_var v pvars =
     if List.mem v pvars then
       []
     else
-      search_in_open_sections (N.Dir_path.repr (Lib.cwd ()))
+      search_in_open_sections (N.DirPath.repr (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
@@ -108,21 +108,21 @@ let ext_of_tag =
 exception FunctorsXMLExportationNotImplementedYet;;
 
 let subtract l1 l2 =
- let l1' = List.rev (Names.Dir_path.repr l1) in
- let l2' = List.rev (Names.Dir_path.repr l2) in
+ let l1' = List.rev (Names.DirPath.repr l1) in
+ let l2' = List.rev (Names.DirPath.repr l2) in
   let rec aux =
    function
       he::tl when tl = l2' -> [he]
     | he::tl -> he::(aux tl)
     | [] -> assert (l2' = []) ; []
   in
-   Names.Dir_path.make (List.rev (aux l1'))
+   Names.DirPath.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.Dir_path.repr dirpath) in
+   List.rev_map N.Id.to_string (N.DirPath.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 fcd01569a..c95cf94b6 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.Dir_path.empty)
+   (N.DirPath.empty)
    (N.Label.make "CProp")
 ;;
 
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 91e15e8a6..033c84691 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.Dir_path.repr modulepath) (List.rev pvars)
+   aux (Names.DirPath.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.Dir_path.make (modules @ N.Dir_path.repr modulepath) in
+         let dirpath = N.DirPath.make (modules @ N.DirPath.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.Dir_path.repr (Lib.library_dp ())) in
+     let toks = List.map N.Id.to_string (N.DirPath.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.rev_map Names.Id.to_string (Names.Dir_path.repr dir))
+    (List.rev_map Names.Id.to_string (Names.DirPath.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.Dir_path.to_string d)))
+       (uri_of_dirpath d) (Names.DirPath.to_string d)))
 ;;