The Coq mailing list

[Julien Tesson <julien.tesson AT univ-orleans.fr>]

Hi list,
we found a very strange "feature" of Coq 8.4 when it comes to evaluate a term 
which relies on type classes, here is a very small example.


Class A :={a : Type}.
Eval compute in a.


Here, [a] evaluate to  [let (a) := ?3 in a : Type] 
whereas in a previous version of Coq (actually 8.3pl3) it fails with message  
"Cannot infer the implicit parameter A of a",  as expected.

If we try to assign the result,
Definition x := Eval compute in a.
it fails, that's why I did'nt call this behaviour a bug, but a (very) strange 
feature.

we were wondering if this behaviour was known and done on purpose ?

Regards,
Julien