diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/search.ml | 2 | ||||
| -rw-r--r-- | vernac/search.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
3 files changed, 6 insertions, 5 deletions
diff --git a/vernac/search.ml b/vernac/search.ml index e1b56b131..540573843 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -367,7 +367,7 @@ let interface_search = let answer = { coq_object_prefix = prefix; coq_object_qualid = qualid; - coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr); + coq_object_object = constr; } in ans := answer :: !ans; in 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} *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 999fe297e..32e18a014 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -39,8 +39,9 @@ module NamedDecl = Context.Named.Declaration let (f_interp_redexp, interp_redexp_hook) = Hook.make () let debug = false -let vernac_prerr_endline x = - if debug then prerr_endline (x ()) else () +(* XXX Should move to a common library *) +let vernac_pperr_endline pp = + if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () (* Misc *) @@ -1933,7 +1934,7 @@ let vernac_load interp fname = * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~loc locality poly c = - vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); match c with (* The below vernac are candidates for removal from the main type and to be put into a new doc_command datatype: *) |