The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

> in a context h1 .. hn |- G, by seeing the targeted hypothesis hi like 
> a goal in the context h1 .. hi-1 |- hi ? 
I strongly doubt it would yield correct tactics (hi is not a consequence 
of the h1...hi-1). However I'd love to see something coming out of it.

> 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...
This is probably because it defines "mytac" as a keyword. I suggest the 
following course of action to get what you want :
Tactic Notation "mytac" := mytac.
Tactic Notation "mytac" "in" hyp(H) := ... .

This should work (by the way "hyp(H)" is better than "ident(H)" for that 
purpose) the way you expect it to.


Arnaud Spiwack