From 347d94a4b966d0cc4a3a04814b0c76c4b05caa11 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 3 Oct 2017 18:58:38 +0200 Subject: Ltac uses the new generic locatable API. --- API/API.ml | 2 +- API/API.mli | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) (limited to 'API') 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/ *) (************************************************************************) -- cgit v1.2.3