The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Dear all,

I'm currently working on polishing my part for the upcoming version of Coq. One common request I got was to bring back the [info] tactical. And, as it happens, I'm now in a situation where I can make it happen.

But what I cannot do, is take the code for the old [info] and port it to the current development version, I really have do write the feature from scratch. And if I get to do [info] anew, I really want to get it right (and possibly divide it in several features).

So, dear [info] user, I'm asking you:

• What do you use [info] for?
• Do you use the [info (info t)] feature?
• If you had one or two feature request for [info] to make it even slightly better, what would they be?
• Is there something which is kind of like [info] but not quite and that you really wished you had in your toolbox?

/Arnaud Spiwack