The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 28.04.2013 23:02, schrieb Gert Smolka:
> I agree that a version of Check that admits existential variables can be 
> useful.  Maybe there should be two versions, one that admits and one that 
> does not admit existential variables.  The command Compute should use the 
> version that disallows existential variables.
>
> I checked Coq 8.3.  There Check and Compute do not admit existential 
> variables.
>
> Gert
>
> On Apr 26, 2013, at 5:04 , Jason Gross 
> <jasongross9 AT gmail.com>
>  wrote:
>
> > I view this as a feature and not a bug.  It may help to [Set Printing All.] 
> > before [Check] to see that Coq fills in existentials for any tems it cannot 
> > infer.  I find it very useful to be able to simplify and check terms with 
> > holes in them, which I often do not yet know how to fill.  If you want to see 
> > if a term is fully filled, you can always do something like [Definition dummy 
> > := f : False. Check @dummy.]
> >
> > -Jason
> >
> > On Apr 22, 2013 4:38 AM, "Gert Smolka" 
> > <smolka AT ps.uni-saarland.de>
> >  wrote:
> > The faulty behavior of Check and Compute appears even with basic queries like
> >
> > Check pair.
> > Compute pair.
> >
> > Gert

Hi all,

I wholeheartedly agree. Considering the amount of confusion the current 
behavior is causing (see, e.g., the mail by Math Prover issued recently) 
and how counter-intuitive it is, I hope that it is changed in a future 
version as described by Mr. Smolka.

Kind regards, Jonas

PS: Sorry for reanimating this thread, but the more I think about it the 
less I can understand why Check and Compute behave like this.