The Coq mailing list

[Stephane Glondu <steph AT glondu.net>]

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.


Cheers,

--
Stéphane