The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

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
>