The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/05/2014 05:12 AM, Arnaud Spiwack wrote:
> Another question: is it useful that [info] be a tactic? Or can it be a
> toplevel command?
>
> If it is useful as a tactic, what should something like [info (t;info u)]
> print?

That depends on what it will do.  If, like the version in PVS (which I 
think just required prefixing a tactic with "@"), it causes the recorded 
script to record the successful low-level tactics instead of the single 
info'ed high-level one, then wouldn't it be beneficial in cases that 
currently use abstract, or maybe in addition to abstract?

If, on the other hand, it just prints things out, then I don't see as 
much benefit to making it a tactic vs. a top-level command.  But it 
might be helpful when debugging a complex tactic to just info certain 
internal components instead of the whole thing.  In that case, [info 
(t;info u)] could act just like [info (t;u)].

-- Jonathan