info_auto tactic does not print traces anymore in Coq8.5?

3
votes

I used to use info_auto to display the steps actually performed under the hood by an auto tactic. However, this no longer seems to work with Coq 8.5 (beta3).

The following example used to work for Coq 8.4:

Example auto_example_5: 2 = 2.
Proof.
  info_auto.
Qed.

and give me the necessary steps such as apply @eq_refl..

With Coq8.5, I get a warning:

The "info_auto" tactic does not print traces anymore. Use "Info 1 auto", instead.
(* info auto : *)

Using Info 1 auto. as hinted, I got:

<unknown>

in the message view. In other occasions, I sometimes get things like 

<unknown>; refine H

But neither is helpful/informational because I can't apply these to finish the proof manually.

What is the proper way to replicate the old info_auto function in Coq 8.5?

1
coqcoq-tactic
I'm also experiencing this. Do you use proof general too or do you get it with coqtop? – dredozubov
Got the same result with coqtop, so i've filed a bug: coq.inria.fr/bugs/show_bug.cgi?id=4587 – dredozubov

1 Answers

2
votes

This issue seems to have been fixed in Coq 8.6.