The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I've submitted a feature request for a flag that toggles this behavior at https://coq.inria.fr/bugs/show_bug.cgi?id=3046.

-Jason

On Sat, May 18, 2013 at 5:43 AM, Jonas Oberhauser <s9joober AT gmail.com> wrote:

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.