The Coq mailing list

[Robbert Krebbers <mail AT robbertkrebbers.nl>]

Hi Enrico,

On 12/21/2015 02:50 PM, Enrico Tassi wrote:
> Or, if you are not afraid of trying an experimental branch, you can
> use /n/ instead of //, where /n/ invokes the user defined ltac ssrdonen
> tactic (n is a number, 0 is reserved).
>
> The branch is called feature/plugin-next on github
>    https://github.com/math-comp/math-comp
> Unfortunately the only doc at the current stage is `git log` and the only
> examples are in the ssrtest disrectory.  Last, it is for 8.5 only.
That is a nice feature!

But I have to say, a number is albeit short not very descriptive. Why 
not also allow /ltac/ where "ltac" can be arbitrary ltac code? I tend to 
write things like:

  rewrite foo by eauto using foo bar baz

Best,

Robbert