Ltac uses the new generic locatable API.

2 files changed, 16 insertions, 1 deletions

diff --git a/API/API.ml b/API/API.ml
index 46ad36d36..bf99d0feb 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -212,7 +212,7 @@ module Pputils = Pputils
 module Ppconstr = Ppconstr
 module Printer = Printer
 (* module Printmod *)
-(* module Prettyp *)
+module Prettyp = Prettyp
 module Ppvernac = Ppvernac
 
 (******************************************************************************)
diff --git a/API/API.mli b/API/API.mli
index e2cb70583..3bd047043 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/                                        *)
 (************************************************************************)