The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Feb 15, 2008, at 10:26 AM, Edsko de Vries wrote:

> On Fri, Feb 15, 2008 at 04:09:40PM +0100, Stephane Glondu wrote:
> > What about:
> >
> > Tactic Notation "rewrite_at" constr(t) constr(t') integer(pos) :=
> >     let H := fresh in
> >     set (H := t) in |- * at pos ;
> >     rewrite t' ;
> >     subst H.
>
> Perfect! Thanks for that. Is that syntax (constr, integer)  
> documented anywhere? I can't find it in the chapter on tactics in  
> the Coq manual.

Take a look at Section 11.4 of the reference manual (at least for Coq  
8.1).  The documentation for Tactic Notation is in there with the  
documentation for Notation.

Cheers,
Brian