The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Fri, Feb 15, 2008 at 10:36:03AM -0500, Brian Aydemir wrote:
> 
> 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.

Ah, right. I was looking in chapter 9 (The Tactic Language).

Thanks,

Edsko