The Coq mailing list

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

On Mon, Dec 21, 2015 at 12:42:39PM +0100, Guillaume Melquiond wrote:
> I suppose you already considered the following solution, but just in
> case you didn't, here it is. While it is a bit more verbose and less
> readable than "by tac", you can use ";[|tac..]" to achieve the same kind
> of goal solving.

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.

Best,
-- 
Enrico Tassi