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

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