The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

2010/10/12 Stéphane Lescuyer 
<stephane.lescuyer AT polytechnique.org>:
>  1 subgoal
>  A : Type
>  EqA : EqDec A
>  x : A
>  y : A
>  H : equal x y = true
> ======================
>  x = y
>> destruct (eq_dec x y).

Hi Stéphane,

I am rather disappointed to find out that this only works in this way
in Coq 8.2.  In Coq 8.3rc1, to achieve the same effect, you must write

destruct (@eq_dec A EqA x y).

While this doesn't entirely negate the usefulness of this technique, I
really wish it was as easy in 8.3 as 8.2.  What happened?  Is there
some new vernacular command I have to use to get 8.3 to cooperate?

 - Aaron