The Coq mailing list

[S3 <scubed2 AT gmail.com>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

> There is no way to ask for this sort of things in Coq v8.3. Simply put,
> the (internal) representation of proofs in progress does not allow to
> express that. After a serious re-engineering, Coq v8.4 has a command Grab 
> Existential Variables, which brings every such hole as a goal. I also have 
> a branch where refine directly exposes all the unsolved holes, but it
> still gives surprising (albeit correct) results when the hole is in a 
> pattern-matching branch (if you want to play with it, you can find the 
> branch on github: https://github.com/aspiwack/coq  (branch new-tacticals)
> ).

Ah, thanks for a complete answer!
I will have to upgrade my version of Coq then.

By exposes all holes, you mean that all holes are added as goals?
Would it be possible to selectively convert from
Existentials into goals?  e.g. say I want have
Existential ?86
It would be convenient if I could just ask for
?86 to be a goal.

- -- 
++++++++++++[->+++++++>+++++++++<<]>-.>[->+>+>+>+>+
<<<<<]>++++++++.>-------.<--.>>.---.>++.>-----.>+++
+++++[->++++<]>.<<<<<<<<.>>++.>.>.>.>>++++++++++.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAlBzl2EACgkQxzVgPqtIcfuU2QCcD01EV2EsAVngrD/JqjolXmPR
L3cAnj3BuiAKlm000GSuZlXtyPOiZbCc
=yzfu
-----END PGP SIGNATURE-----