The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Scott and sorry for the late answer,

The info_auto tactic has just been fixed by Hugo and thus should work normally in 8.5pl3 (whenever there is such a thing) and in 8.6beta (which should arrive quite soon). You can also compile the 8.5 branch yourself.

In the meantime, note that there also exists a `debug auto` tactic, which is a bit more verbose because it shows also the tentative proofs that failed.

Cheers,

Théo

Le jeu. 24 mars 2016 à 04:41, scott constable <sdconsta AT syr.edu> a écrit :

Hi All,

I recently stumbled upon the info_eauto tactic on a forum, and have found it very useful. For instance, running

Hint Constructors or.

Example easyy : forall p q, p /\ q -> q /\ p.

Proof. intros. destruct H. info_eauto.

prints this very helpful output:

Debug: (* info eauto : *)

Debug: apply conj.

Debug:  exact H0.

Debug:  exact H.

My first question is, why isn't this tactic in the 8.5 manual?

Second, one would expect that if there is an info_eauto, then there should also be an info_auto, but when I try to invoke info_auto, coq reports:

Warning: The "info_auto" tactic does not print traces anymore. Use "Info 1

 auto", instead.

But the output from "Info 1 auto" tends to be incredibly unhelpful. Using "Info 1 auto" in place of "info_eauto" in the same example from above yields:

<unknown>;[> refine H0 | refine H ]

which is certainly not very enlightening. So why is there no info_auto?

~Scott Constable