The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Yes.

It's occasionally useful to be able to compute with existential variables.

Why is it strange ?

On 10 October 2012 23:28, Julien Tesson <julien.tesson AT univ-orleans.fr> wrote:

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