The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 24/01/2015 22:38, Jonathan Leivent wrote:
> [Requesting a fix to this will result in some Coq developer informing
> you that Tactic Notation is an abomination.]

Me, most probably. And indeed, this is an abomination. It does not hurt
to remind it to the face of the earth.

That said though, I do have future plans to try to fix the tactic
notation mechanism, making it true notations (and thus breaking all
hackish code relying on it, you've been warned). But that's a long-term
task...

Anyway, I recommend the use of ML-level tactics in this case instead of
ugly hacks, now that in 8.5 the former were tweaked to respect the
module scoping system.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature