From f42dd8d8530e6227621ccd662741f1da23700304 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 library/libnames.mli | 52 +++++++++++++++++++++++++++-------------------------
 1 file changed, 27 insertions(+), 25 deletions(-)

(limited to 'library/libnames.mli')

diff --git a/library/libnames.mli b/library/libnames.mli
index 08330349e..090709549 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -11,31 +11,33 @@ open Loc
 open Names
 
 (** {6 Dirpaths } *)
-val pr_dirpath : dir_path -> Pp.std_ppcmds
+(** FIXME: ought to be in Names.dir_path *)
 
-val dirpath_of_string : string -> dir_path
-val string_of_dirpath : dir_path -> string
+val pr_dirpath : Dir_path.t -> Pp.std_ppcmds
 
-(** Pop the suffix of a [dir_path] *)
-val pop_dirpath : dir_path -> dir_path
+val dirpath_of_string : string -> Dir_path.t
+val string_of_dirpath : Dir_path.t -> string
+
+(** Pop the suffix of a [Dir_path.t] *)
+val pop_dirpath : Dir_path.t -> Dir_path.t
 
 (** Pop the suffix n times *)
-val pop_dirpath_n : int -> dir_path -> dir_path
+val pop_dirpath_n : int -> Dir_path.t -> Dir_path.t
 
-(** Give the immediate prefix and basename of a [dir_path] *)
-val split_dirpath : dir_path -> dir_path * Id.t
+(** Give the immediate prefix and basename of a [Dir_path.t] *)
+val split_dirpath : Dir_path.t -> Dir_path.t * Id.t
 
-val add_dirpath_suffix : dir_path -> module_ident -> dir_path
-val add_dirpath_prefix : module_ident -> dir_path -> dir_path
+val add_dirpath_suffix : Dir_path.t -> module_ident -> Dir_path.t
+val add_dirpath_prefix : module_ident -> Dir_path.t -> Dir_path.t
 
-val chop_dirpath : int -> dir_path -> dir_path * dir_path
-val append_dirpath : dir_path -> dir_path -> dir_path
+val chop_dirpath : int -> Dir_path.t -> Dir_path.t * Dir_path.t
+val append_dirpath : Dir_path.t -> Dir_path.t -> Dir_path.t
 
-val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
-val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+val drop_dirpath_prefix : Dir_path.t -> Dir_path.t -> Dir_path.t
+val is_dirpath_prefix_of : Dir_path.t -> Dir_path.t -> bool
 
-module Dirset : Set.S with type elt = dir_path
-module Dirmap : Map.S with type key = dir_path
+module Dirset : Set.S with type elt = Dir_path.t
+module Dirmap : Map.S with type key = Dir_path.t
 
 (** {6 Full paths are {e absolute} paths of declarations } *)
 type full_path
@@ -43,11 +45,11 @@ type full_path
 val eq_full_path : full_path -> full_path -> bool
 
 (** Constructors of [full_path] *)
-val make_path : dir_path -> Id.t -> full_path
+val make_path : Dir_path.t -> Id.t -> full_path
 
 (** Destructors of [full_path] *)
-val repr_path : full_path -> dir_path * Id.t
-val dirpath : full_path -> dir_path
+val repr_path : full_path -> Dir_path.t * Id.t
+val dirpath : full_path -> Dir_path.t
 val basename : full_path -> Id.t
 
 (** Parsing and printing of section path as ["coq_root.module.id"] *)
@@ -67,8 +69,8 @@ val restrict_path : int -> full_path -> full_path
 
 type qualid
 
-val make_qualid : dir_path -> Id.t -> qualid
-val repr_qualid : qualid -> dir_path * Id.t
+val make_qualid : Dir_path.t -> Id.t -> qualid
+val repr_qualid : qualid -> Dir_path.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
@@ -80,7 +82,7 @@ val qualid_of_string : string -> qualid
    qualified name denoting the same name *)
 
 val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : dir_path -> qualid
+val qualid_of_dirpath : Dir_path.t -> qualid
 val qualid_of_ident : Id.t -> qualid
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
@@ -89,19 +91,19 @@ val qualid_of_ident : Id.t -> qualid
 
 type object_name = full_path * kernel_name
 
-type object_prefix = dir_path * (module_path * dir_path)
+type object_prefix = Dir_path.t * (module_path * Dir_path.t)
 
 val eq_op : object_prefix -> object_prefix -> bool
 
 val make_oname : object_prefix -> Id.t -> object_name
 
-(** to this type are mapped [dir_path]'s in the nametab *)
+(** to this type are mapped [Dir_path.t]'s in the nametab *)
 type global_dir_reference =
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of dir_path
+  | DirClosedSection of Dir_path.t
       (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
-- 
cgit v1.2.3