diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-08 18:13:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:51:47 +0100 |
| commit | 921ea3983d45051ae85b0e20bf13de2eff38e53e (patch) | |
| tree | 6b8a7f33e7df5d2eac0c81a8839ca6d749fad752 /vernac/search.ml | |
| parent | 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 (diff) | |
[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.
Diffstat (limited to 'vernac/search.ml')
| -rw-r--r-- | vernac/search.ml | 2 |
1 files changed, 1 insertions, 1 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 |