From 921ea3983d45051ae85b0e20bf13de2eff38e53e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Feb 2017 18:13:25 +0100 Subject: [pp] Remove uses of expensive string_of_ppcmds. In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself. --- vernac/search.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/search.mli') diff --git a/vernac/search.mli b/vernac/search.mli index c9167c485..82b79f75d 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -67,7 +67,7 @@ type 'a coq_object = { } val interface_search : ?glnum:int -> (search_constraint * bool) list -> - string coq_object list + constr coq_object list (** {6 Generic search function} *) -- cgit v1.2.3