The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/24/2015 06:53 PM, Pierre-Marie Pédrot wrote:
> 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

Will there be documentation on ML-level tactics, instead of merely 
pointing out some github project that is several years out of date, and 
lacking in sufficient detail regardless?  That is all I received the 
last time I asked.

As for those hacks - I was hoping that their ugliness - which is 
required to accomplish such tasks entirely in Ltac as it stands - would 
perhaps help instigate better Ltac constructs and design. After all, it 
is one thing to say "it would be nice if", but perhaps more encouraging 
of change to say "look how useful this is, though it is painful to look 
at, and probably unmaintainable".  The second also allows progress while 
waiting for change.

But, I will do both.  The first did succeed in getting "multimatch" - 
although perhaps because that was easy due to how match already was 
implemented.  I'll even learn how to write ML-level tactics, once the 
proper doc is made available.

-- Jonathan