From 267c880c5e8b73770316518a2a820e779c121fdb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 3 Oct 2016 16:09:03 +0200
Subject: Exporting Nametab generic API.

---
 library/nametab.mli | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

(limited to 'library')

diff --git a/library/nametab.mli b/library/nametab.mli
index d20c399b60..3d90e1b5a5 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -173,3 +173,36 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
 
 val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
 val absolute_reference : full_path -> global_reference (** = global_of_path *)
+
+(** Generic name handling *)
+
+module type UserName = sig
+  type t
+  val equal : t -> t -> bool
+  val to_string : t -> string
+  val repr : t -> Id.t * module_ident list
+end
+
+module type EqualityType =
+sig
+  type t
+  val equal : t -> t -> bool
+end
+
+module type NAMETREE = sig
+  type elt
+  type t
+  type user_name
+
+  val empty : t
+  val push : visibility -> user_name -> elt -> t -> t
+  val locate : qualid -> t -> elt
+  val find : user_name -> t -> elt
+  val exists : user_name -> t -> bool
+  val user_name : qualid -> t -> user_name
+  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val find_prefixes : qualid -> t -> elt list
+end
+
+module Make (U : UserName) (E : EqualityType) :
+  NAMETREE with type user_name = U.t and type elt = E.t
-- 
cgit v1.2.3


From 37e84b83739fec666264904bc06fd32b46b83140 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 18 May 2017 14:51:03 +0200
Subject: Adding a trespasser warning to the Nametab API.

---
 library/nametab.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/nametab.mli b/library/nametab.mli
index 3d90e1b5a5..095ac4f9df 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -174,7 +174,9 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
 val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
 val absolute_reference : full_path -> global_reference (** = global_of_path *)
 
-(** Generic name handling *)
+(** {5 Generic name handling} *)
+
+(** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)
 
 module type UserName = sig
   type t
-- 
cgit v1.2.3