The Coq mailing list

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

On Fri, Feb 15, 2008 at 04:09:40PM +0100, Stephane Glondu wrote:
> Edsko de Vries a écrit :
> >which is reasonably nice (we should introduce some custom notation,
> >perhaps). It would be nicer if we should pass in a position, but
> >unfortunately if we define
> >
> >  Ltac rewrite_at t t' pos := 
> >    let H := fresh in
> >    set (H := t) in |- * at pos ;
> >    rewrite t' ;
> >    subst H.
> >
> >then
> >  
> >  rewrite_at a ab 1.
> >
> >gives
> >
> >  User error: Ltac variable pos is bound to a term
> >    which cannot be coerced to an integer
> 
> 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.

Edkso