The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 12 Oct 2012 15:00:21 +0200,
Julien Tesson 
<julien.tesson AT univ-orleans.fr>
 a écrit :

> Le 11/10/2012 10:47, Arnaud Spiwack a écrit :
> > Yes.
> >
> > It's occasionally useful to be able to compute with existential
> > variables.
> >
> > Why is it strange ?
> It looked strange for me at first because I would have expected the
> same behaviour (in term of failure) between  [Eval compute in a] and
> [Definition x := Eval compute in a], and because when I use type
> classes, I expect that the instance search mechanism warn me when it
> failed to find a matching instance.
> 
> This new behaviour seems interesting  but I found it surprising at
> first.
> 
> Regards,
> Julien

I guess "Definition x := Eval compute in a" could be made to work by
automatically generalizing existentials, buth then I fear it would
become hard to predict what really will x be.