Imported Upstream version 8.5~beta1+dfsg

1 files changed, 27 insertions, 22 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index 79ea119b..e3aeb675 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -1,15 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Pp
 open Names
 open Libnames
+open Globnames
 
 (** This module contains the tables for globalization. *)
 
@@ -17,7 +17,7 @@ open Libnames
     qualified names (qualid). There are three classes of names:
 
     - 1a) internal kernel names: [kernel_name], [constant], [inductive],
-         [module_path], [dir_path]
+         [module_path], [DirPath.t]
 
     - 1b) other internal names: [global_reference], [syndef_name],
         [extended_global_reference], [global_dir_reference], ...
@@ -33,7 +33,7 @@ open Libnames
 
      Registers the [object_reference] to be referred to by the
      [full_user_name] (and its suffixes according to [visibility]).
-     [full_user_name] can either be a [full_path] or a [dir_path].
+     [full_user_name] can either be a [full_path] or a [DirPath.t].
    }
    {- [exists : full_user_name -> bool]
 
@@ -51,19 +51,17 @@ open Libnames
    {- [shortest_qualid_of : object_reference -> user_name]
 
      The [user_name] can be for example the shortest non ambiguous [qualid] or
-     the [full_user_name] or [identifier]. Such a function can also have a
+     the [full_user_name] or [Id.t]. Such a function can also have a
      local context argument.}}
 
 *)
 
 
 exception GlobalizationError of qualid
-exception GlobalizationConstantError of qualid
 
 (** Raises a globalization error *)
-val error_global_not_found_loc : loc -> qualid -> 'a
+val error_global_not_found_loc : Loc.t -> qualid -> 'a
 val error_global_not_found     : qualid -> 'a
-val error_global_constant_not_found_loc : loc -> qualid -> 'a
 
 (** {6 Register visibility of things } *)
 
@@ -79,7 +77,7 @@ type visibility = Until of int | Exactly of int
 
 val push : visibility -> full_path -> global_reference -> unit
 val push_modtype : visibility -> full_path -> module_path -> unit
-val push_dir : visibility -> dir_path -> global_dir_reference -> unit
+val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
 type ltac_constant = kernel_name
@@ -98,7 +96,7 @@ val locate_syndef : qualid -> syndef_name
 val locate_modtype : qualid -> module_path
 val locate_dir : qualid -> global_dir_reference
 val locate_module : qualid -> module_path
-val locate_section : qualid -> dir_path
+val locate_section : qualid -> DirPath.t
 val locate_tactic : qualid -> ltac_constant
 
 (** These functions globalize user-level references into global
@@ -113,6 +111,9 @@ val global_inductive : reference -> inductive
 
 val locate_all : qualid -> global_reference list
 val locate_extended_all : qualid -> extended_global_reference list
+val locate_extended_all_tactic : qualid -> ltac_constant list
+val locate_extended_all_dir : qualid -> global_dir_reference list
+val locate_extended_all_modtype : qualid -> module_path list
 
 (** Mapping a full path to a global reference *)
 
@@ -123,15 +124,16 @@ val extended_global_of_path : full_path -> extended_global_reference
 
 val exists_cci : full_path -> bool
 val exists_modtype : full_path -> bool
-val exists_dir : dir_path -> bool
-val exists_section : dir_path -> bool (** deprecated synonym of [exists_dir] *)
-val exists_module : dir_path -> bool (** deprecated synonym of [exists_dir] *)
+val exists_dir : DirPath.t -> bool
+val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *)
+val exists_tactic : full_path -> bool (** deprecated synonym of [exists_dir] *)
 
 (** {6 These functions locate qualids into full user names } *)
 
 val full_name_cci : qualid -> full_path
 val full_name_modtype : qualid -> full_path
-val full_name_module : qualid -> dir_path
+val full_name_module : qualid -> DirPath.t
 
 (** {6 Reverse lookup }
   Finding user names corresponding to the given
@@ -142,25 +144,28 @@ val full_name_module : qualid -> dir_path
 
 val path_of_syndef : syndef_name -> full_path
 val path_of_global : global_reference -> full_path
-val dirpath_of_module : module_path -> dir_path
+val dirpath_of_module : module_path -> DirPath.t
+val path_of_modtype : module_path -> full_path
 val path_of_tactic : ltac_constant -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
 
-val dirpath_of_global : global_reference -> dir_path
-val basename_of_global : global_reference -> identifier
+val dirpath_of_global : global_reference -> DirPath.t
+val basename_of_global : global_reference -> Id.t
 
-(** Printing of global references using names as short as possible *)
-val pr_global_env : Idset.t -> global_reference -> std_ppcmds
+(** Printing of global references using names as short as possible.
+    @raise Not_found when the reference is not in the global tables. *)
+val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds
 
 
 (** The [shortest_qualid] functions given an object with [user_name]
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
-   Coq.A.B.x that denotes the same object. *)
+   Coq.A.B.x that denotes the same object.
+   @raise Not_found for unknown objects. *)
 
-val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid
+val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
+val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : module_path -> qualid
 val shortest_qualid_of_module : module_path -> qualid
 val shortest_qualid_of_tactic : ltac_constant -> qualid