The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello,

For the 8.3 release there was a change in the semantics of Ltac match as it pertains to unification variables. In 8.2 and before, if X referred to a unification variable, then

match X with

  | X => idtac

end

would fail. This was viewed as a bug and changed in: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2433

The old behavior seems to be back in 8.3pl4:

Goal exists x : nat, x = x.

  eexists.

  match goal with

    | [ |- ?X = ?Y ] =>

      match X with

        | Y => idtac "matched! Y"

        | X => idtac "matched! X"

        | _ => idtac "didn't match!"

      end

  end.

prints out "didn't match".

Thanks.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/