The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Feb 27, 2015 at 12:13:30PM +0100, Pierre-Marie Pédrot wrote:
> The more I see the horrendous hacks people build up using tactics in
> terms, the more I regret having introduced this feature without thinking
> twice about how people use Ltac.

You are still in time to take it back (disable it) if you think it is
not "ready to be maintained".

I'm a fan of it, I've always wanted it in Matita.  But if such feature
interacts too badly with Ltac, it may be wise not to let people open the
box of Pandora.

My2C.
-- 
Enrico Tassi