The Coq mailing list

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

On Mon, Dec 21, 2015 at 02:54:53PM +0100, Robbert Krebbers wrote:
> 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

In that case I would suggest something along the lines of what Guillaume
proposes:
 
    rewrite foo; last by eauto using foo bar baz.

(It could be "first by ...", I don't recall now).

The // is a short expression to quickly kill sub goals, and continue the
rewrite line.  Writing an ltac in there seems to go in a completely
different direction.

Best,
-- 
Enrico Tassi