The Coq mailing list

[frederic.blanqui AT loria.fr]

On Thu, 29 May 2008, Andrew McCreight wrote:

> This might not be quite what you are looking for, but you can manually
> define a variant of your tactic with "in" using Tactic Notation.
>
> For a number of examples, look here:
>
> http://logical.futurs.inria.fr/cocorico/Folding%20tactics

thank you very much for this tip. unfortunately, it does not work:

Ltac mytac := ...

Tactic Notation "mytac" "in" ident(H) := ...

after this tactic definition, it seems that "mytac" must always be followed by 
"in". otherwise we get a syntax error.

in built-in tactics, the "in" is optional...