The Coq mailing list

[Paul van Wamelen <wamelen AT marais.math.lsu.edu>]

Dear coq-club,

Is the following a bug?

1 subgoal

  U : Type
  Gr : (Group U)
  x : U
  InGx : (In U G x)
  x0 : U
  eq1 : (star x e x0)
  ============================
   (star x e x)

r_ntrl < Replace x0 with x in eq1.
Toplevel input, characters 18-20
> Replace x0 with x in eq1.
>                   ^^
Syntax error: '.' expected after [Vernac.tacarg] (in [Vernac.vernac])

Of course this can be done with
  Cut x==x0.
  Intro eq2.
  Rewrite <- eq2 in eq1.

but the documentation does say that Replace _ with _ in _ should work.

Another question: Is there a way of "Replace"ing (or "Rewrite"ing)
only the second x in (star x e x) with x0?

I'm using the binary distribution, V6.2, on a Sparc/Solaris. Is a
binary of V6.2.1 available yet (at http://pauillac.inria.fr/coq/ I
only see coq-6.2-solaris-sparc.tar.gz)?

Sincerely,
Paul van Wamelen.