Modulification of identifier

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

1 files changed, 18 insertions, 18 deletions

diff --git a/library/lib.mli b/library/lib.mli
index 25c0e1b24..75e18b194 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -27,7 +27,7 @@ type node =
 
 and library_segment = (Libnames.object_name * node) list
 
-type lib_objects = (Names.identifier * Libobject.obj) list
+type lib_objects = (Names.Id.t * Libobject.obj) list
 
 (** {6 Object iteration functions. } *)
 
@@ -53,12 +53,12 @@ val segment_of_objects :
 (** Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
-val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
+val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
 val add_anonymous_leaf : Libobject.obj -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
-val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
+val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name
 
 val add_frozen_state : unit -> unit
 
@@ -75,14 +75,14 @@ val contents_after : Libnames.object_name option -> library_segment
 val cwd : unit -> Names.dir_path
 val cwd_except_section : unit -> Names.dir_path
 val current_dirpath : bool -> Names.dir_path (* false = except sections *)
-val make_path : Names.identifier -> Libnames.full_path
-val make_path_except_section : Names.identifier -> Libnames.full_path
+val make_path : Names.Id.t -> Libnames.full_path
+val make_path_except_section : Names.Id.t -> Libnames.full_path
 val path_of_include : unit -> Libnames.full_path
 
 (** Kernel-side names *)
 val current_prefix : unit -> Names.module_path * Names.dir_path
-val make_kn : Names.identifier -> Names.kernel_name
-val make_con : Names.identifier -> Names.constant
+val make_kn : Names.Id.t -> Names.kernel_name
+val make_con : Names.Id.t -> Names.constant
 
 (** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -98,7 +98,7 @@ val is_module : unit -> bool
 val current_mod_id : unit -> Names.module_ident
 
 (** Returns the opening node of a given name *)
-val find_opening_node : Names.identifier -> node
+val find_opening_node : Names.Id.t -> node
 
 (** {6 Modules and module types } *)
 
@@ -134,13 +134,13 @@ val library_dp : unit -> Names.dir_path
 (** Extract the library part of a name even if in a section *)
 val dp_of_mp : Names.module_path -> Names.dir_path
 val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
-val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
+val split_modpath : Names.module_path -> Names.dir_path * Names.Id.t list
 val library_part :  Globnames.global_reference -> Names.dir_path
 val remove_section_part : Globnames.global_reference -> Names.dir_path
 
 (** {6 Sections } *)
 
-val open_section : Names.identifier -> unit
+val open_section : Names.Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 Backtracking } *)
@@ -164,7 +164,7 @@ val first_command_label : int
 val reset_label : int -> unit
 
 (** search the label registered immediately before adding some definition *)
-val label_before_name : Names.identifier Loc.located -> int
+val label_before_name : Names.Id.t Loc.located -> int
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
 
@@ -176,29 +176,29 @@ val unfreeze : frozen -> unit
 val init : unit -> unit
 
 (** XML output hooks *)
-val set_xml_open_section : (Names.identifier -> unit) -> unit
-val set_xml_close_section : (Names.identifier -> unit) -> unit
+val set_xml_open_section : (Names.Id.t -> unit) -> unit
+val set_xml_close_section : (Names.Id.t -> unit) -> unit
 
 (** {6 Section management for discharge } *)
-type variable_info = Names.identifier * Decl_kinds.binding_kind *
+type variable_info = Names.Id.t * Decl_kinds.binding_kind *
     Term.constr option * Term.types
 type variable_context = variable_info list
 
-val instance_from_variable_context : variable_context -> Names.identifier array
+val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Sign.named_context
 
 val section_segment_of_constant : Names.constant -> variable_context
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
 
-val section_instance : Globnames.global_reference -> Names.identifier array
+val section_instance : Globnames.global_reference -> Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> Decl_kinds.binding_kind -> unit
+val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> unit
 
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
 val replacement_context : unit ->
-  (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t)
+  (Names.Id.t array Names.Cmap.t * Names.Id.t array Names.Mindmap.t)
 
 (** {6 Discharge: decrease the section level if in the current section } *)