The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Many times, the following tactic succeeds:

assert (a=b) by reflexivity.

but the following fails with some type inference error suggesting that
while inferring types, Coq is not exploiting the fact that `a` and `b`
must have the same types:

change a with b

Can the `change` tactic be made as smart as `assert (_=_)`?

I thought the following Ltac would work, but it suffers from the same
problem as `change`.
      Ltac changee a b :=
        assert (a=b) as XX by reflexivity;
        rewrite XX;
        clear XX.

I guess terms are fully typed before being passed to Ltac.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/