empty response for info_auto tactic

[yaitskov]

Hi,

info_auto tactic runs auto tactic with logging but the *response* buffer is empty.

coqtop output:

(* info auto: *)
intro.
intro.
intro.
intro.
intro.
simple apply or_intror (in core).
simple apply conj (in core).
assumption.
simple apply H0.
assumption.
coq-core.plugins.ltac::auto@0
No more goals.

GNU Emacs 30.2 (build 1, x86_64-pc-linux-gnu, X toolkit, cairo version 1.18.4, Xaw3d scroll bars)
Version 4.6-git

[hendriktews]

Thanks for the report. When I try info_auto in one example the info auto output shows up in the response buffer. Which version of PG and Coq/Rocq are you using? Can you upload an example that reliably reproduces the problem for you?