The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

Don't worry, it's just Bug #2222 :-) it has been corrected last week
only, so it was still there in the release candidate. The trunk
version of branch 8.3 should be ok.

Stéphane

2010/10/13 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
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06