Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de DischargeAt)

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

1 files changed, 34 insertions, 15 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index 84b25d9cd6..1e1b4cb3f3 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -10,19 +10,22 @@ open Pp
 type identifier
 type name = Name of identifier | Anonymous
 
+(* Constructor of an identifier;
+   [make_ident] builds an identifier from a string and an index; if
+   the string ends by a digit, a "_" is inserted *)
 val make_ident : string -> int -> identifier
-val string_of_id : identifier -> string
-val id_of_string : string -> identifier
 
-val explode_id : identifier -> string list
-val print_id : identifier -> std_ppcmds
-val print_idl : identifier list -> std_ppcmds
+(* Some destructors of an identifier *)
 val atompart_of_id : identifier -> string
-val index_of_id : identifier -> int
-val id_ord : identifier -> identifier -> int
-val id_without_number : identifier -> bool
 val first_char : identifier -> string
+val index_of_id : identifier -> int
+
+(* Parsing and printing of identifiers *)
+val string_of_id : identifier -> string
+val id_of_string : string -> identifier
+val print_id : identifier -> std_ppcmds
 
+(* Identifiers sets and maps *)
 module Idset : Set.S with type elt = identifier
 module Idmap : Map.S with type key = identifier
 
@@ -32,32 +35,42 @@ val next_ident_away : identifier -> identifier list -> identifier
 val next_name_away : name -> identifier list -> identifier
 val next_name_away_with_default : 
   string -> name -> identifier list -> identifier
-val get_new_ids : int -> identifier -> identifier list -> identifier list
-
-val id_of_name : identifier -> name -> identifier
 
+(*s path_kind is currently degenerated, only [CCI] is used *)
 type path_kind = CCI | FW | OBJ
 
+(* parsing and printing of path kinds *)
 val string_of_kind : path_kind -> string
 val kind_of_string : string -> path_kind
 
+(*s Directory paths = section names paths *)
+type dir_path = string list
+
+(* Printing of directory paths as "#module#submodule" *)
+val string_of_dirpath : dir_path -> string
+
 (*s Section paths *)
 type section_path
 
-val make_path : string list -> identifier -> path_kind -> section_path
-val repr_path : section_path -> string list * identifier * path_kind
-val dirpath : section_path -> string list
+(* Constructors of [section_path] *)
+val make_path : dir_path -> identifier -> path_kind -> section_path
+
+(* Destructors of [section_path] *)
+val repr_path : section_path -> dir_path * identifier * path_kind
+val dirpath : section_path -> dir_path
 val basename : section_path -> identifier
 val kind_of_path : section_path -> path_kind
 
 val sp_of_wd : string list -> section_path
 val wd_of_sp : section_path -> string list
 
+(* Parsing and printing of section path as "#module#id#kind" *)
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
-val string_of_path_mind : section_path -> identifier -> string
 val print_sp : section_path -> std_ppcmds
 
+(*
+val string_of_path_mind : section_path -> identifier -> string
 val coerce_path : path_kind -> section_path -> section_path
 val fwsp_of : section_path -> section_path
 val ccisp_of : section_path -> section_path
@@ -68,8 +81,13 @@ val append_to_path : section_path -> string -> section_path
 
 val sp_ord : section_path -> section_path -> int
 val sp_gt : section_path * section_path -> bool
+*)
 
+(* [is_dirpath_prefix p1 p2=true] if [p1] is a prefix of or is equal to [p2] *)
+val dirpath_prefix_of : dir_path -> dir_path -> bool
+(*
 module Spset : Set.S with type elt = section_path
+*)
 module Spmap : Map.S with type key = section_path
 
 (*s Specific paths for declarations *)
@@ -80,3 +98,4 @@ type constructor_path = inductive_path * int
 val hcons_names : unit ->
   (section_path -> section_path) * (section_path -> section_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
+