From 267c880c5e8b73770316518a2a820e779c121fdb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/nametab.mli')

diff --git a/library/nametab.mli b/library/nametab.mli
index d20c399b6..3d90e1b5a 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