Ltac uses the new generic locatable API.

1 files changed, 15 insertions, 0 deletions

diff --git a/API/API.mli b/API/API.mli
index e2cb70583d..3bd047043a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5005,6 +5005,21 @@ sig
   val pr_transparent_state : Names.transparent_state -> Pp.t
 end
 
+module Prettyp :
+sig
+  type 'a locatable_info = {
+    locate : Libnames.qualid -> 'a option;
+    locate_all : Libnames.qualid -> 'a list;
+    shortest_qualid : 'a -> Libnames.qualid;
+    name : 'a -> Pp.t;
+    print : 'a -> Pp.t;
+    about : 'a -> Pp.t;
+  }
+
+  val register_locatable : string -> 'a locatable_info -> unit
+  val print_located_other : string -> Libnames.reference -> Pp.t
+end
+
 (************************************************************************)
 (* End of modules from printing/                                        *)
 (************************************************************************)