From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 library/libnames.mli | 46 +++++++++++-----------------------------------
 1 file changed, 11 insertions(+), 35 deletions(-)

(limited to 'library/libnames.mli')

diff --git a/library/libnames.mli b/library/libnames.mli
index 9dad2612..447eecbb 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -14,12 +14,6 @@ open Names
 (** {6 Dirpaths } *)
 val dirpath_of_string : string -> DirPath.t
 
-val pr_dirpath : DirPath.t -> Pp.t
-[@@ocaml.deprecated "Alias for DirPath.print"]
-
-val string_of_dirpath : DirPath.t -> string
-[@@ocaml.deprecated "Alias for DirPath.to_string"]
-
 (** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *)
 val pop_dirpath : DirPath.t -> DirPath.t
 
@@ -71,23 +65,28 @@ val restrict_path : int -> full_path -> full_path
     qualifications of absolute names, including single identifiers.
     The [qualid] are used to access the name table. *)
 
-type qualid
+type qualid_r
+type qualid = qualid_r CAst.t
 
-val make_qualid : DirPath.t -> Id.t -> qualid
+val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid
 val repr_qualid : qualid -> DirPath.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
 val pr_qualid : qualid -> Pp.t
 val string_of_qualid : qualid -> string
-val qualid_of_string : string -> qualid
+val qualid_of_string : ?loc:Loc.t -> string -> qualid
 
 (** Turns an absolute name, a dirpath, or an Id.t into a
    qualified name denoting the same name *)
 
-val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : DirPath.t -> qualid
-val qualid_of_ident : Id.t -> qualid
+val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
+val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
+val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+
+val qualid_is_ident : qualid -> bool
+val qualid_path : qualid -> DirPath.t
+val qualid_basename : qualid -> Id.t
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
    can be substituted and a "syntactic" [full_path] which can be printed
@@ -125,27 +124,11 @@ type global_dir_reference =
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of DirPath.t
-      (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
   global_dir_reference -> global_dir_reference -> bool
 
 (** {6 ... } *)
-(** A [reference] is the user-level notion of name. It denotes either a
-    global name (referred either by a qualified name or by a single
-    name) or a variable *)
-
-type reference_r =
-  | Qualid of qualid
-  | Ident of Id.t
-type reference = reference_r CAst.t
-
-val eq_reference : reference -> reference -> bool
-val qualid_of_reference : reference -> qualid CAst.t
-val string_of_reference : reference -> string
-val pr_reference : reference -> Pp.t
-val join_reference : reference -> reference -> reference
 
 (** some preset paths *)
 val default_library : DirPath.t
@@ -157,10 +140,3 @@ val coq_string : string (** "Coq" *)
 (** This is the default root prefix for developments which doesn't
    mention a root *)
 val default_root_prefix : DirPath.t
-
-(** Deprecated synonyms *)
-val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *)
-[@@ocaml.deprecated "Alias for qualid_of_ident"]
-
-val qualid_of_sp : full_path -> qualid (** = qualid_of_path *)
-[@@ocaml.deprecated "Alias for qualid_of_sp"]
-- 
cgit v1.2.3