The Coq mailing list

[Luke Maurer <maurerl AT cs.uoregon.edu>]

When I saw that info wasn't working in 8.4beta, I figured it was a beta 
thing, but then I re-read the CHANGES file and became very sad :-(

> - Support for tactical "info" is suspended.

As a devoted Adamizer of proof scripts (with a summer's worth of 
Ltackery to prove it), I can't imagine life without info ...

I assume this is a consequence of the new proof engine? Is there any 
hope that info could be restored before the 8.4 final release? If it's a 
matter of manpower, is adapting info to the new engine something a lowly 
master's student might be helpful for? I've been toying with writing a 
few (very simple) ML tactics, so I've probably at least *seen* a few of 
the files involved :-)

--
- Luke