From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 library/libnames.mli | 72 +++++++++++++++++++++++++++++++++++++---------------
 1 file changed, 52 insertions(+), 20 deletions(-)

(limited to 'library/libnames.mli')

diff --git a/library/libnames.mli b/library/libnames.mli
index 58d1da9d..9dad2612 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -1,23 +1,24 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Util
-open Pp
-open Loc
 open Names
 
 (** {6 Dirpaths } *)
-(** FIXME: ought to be in Names.dir_path *)
+val dirpath_of_string : string -> DirPath.t
 
-val pr_dirpath : DirPath.t -> Pp.std_ppcmds
+val pr_dirpath : DirPath.t -> Pp.t
+[@@ocaml.deprecated "Alias for DirPath.print"]
 
-val dirpath_of_string : string -> DirPath.t
 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
@@ -58,7 +59,7 @@ val basename : full_path -> Id.t
 (** Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> full_path
 val string_of_path : full_path -> string
-val pr_path : full_path -> std_ppcmds
+val pr_path : full_path -> Pp.t
 
 module Spmap  : CSig.MapS with type key = full_path
 
@@ -77,7 +78,7 @@ val repr_qualid : qualid -> DirPath.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
-val pr_qualid : qualid -> std_ppcmds
+val pr_qualid : qualid -> Pp.t
 val string_of_qualid : qualid -> string
 val qualid_of_string : string -> qualid
 
@@ -92,9 +93,27 @@ val qualid_of_ident : Id.t -> qualid
    can be substituted and a "syntactic" [full_path] which can be printed
 *)
 
-type object_name = full_path * kernel_name
+type object_name = full_path * KerName.t
+
+(** Object prefix morally contains the "prefix" naming of an object to
+   be stored by [library], where [obj_dir] is the "absolute" path,
+   [obj_mp] is the current "module" prefix and [obj_sec] is the
+   "section" prefix.
+
+    Thus, for an object living inside [Module A. Section B.] the
+   prefix would be:
+
+    [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ]
+
+    Note that both [obj_dir] and [obj_sec] are "paths" that is to say,
+   as opposed to [obj_mp] which is a single module name.
 
-type object_prefix = DirPath.t * (module_path * DirPath.t)
+ *)
+type object_prefix = {
+  obj_dir : DirPath.t;
+  obj_mp  : ModPath.t;
+  obj_sec : DirPath.t;
+}
 
 val eq_op : object_prefix -> object_prefix -> bool
 
@@ -117,18 +136,31 @@ val eq_global_dir_reference :
     global name (referred either by a qualified name or by a single
     name) or a variable *)
 
-type reference =
-  | Qualid of qualid located
-  | Ident of Id.t located
+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 located
+val qualid_of_reference : reference -> qualid CAst.t
 val string_of_reference : reference -> string
-val pr_reference : reference -> std_ppcmds
-val loc_of_reference : reference -> Loc.t
+val pr_reference : reference -> Pp.t
 val join_reference : reference -> reference -> reference
 
-(** Deprecated synonyms *)
+(** some preset paths *)
+val default_library : DirPath.t
+
+(** This is the root of the standard library of Coq *)
+val coq_root : module_ident (** "Coq" *)
+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