The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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.

I suppose it would be possible, but I haven't implemented it yet. Part of the problem is how to name, on the user side, existential variable: you cannot use the displayed name as it is not stable, that's why the instantiate tactics count them from 1, but it always seemed unsatisfactory to me (in particular, I tended to get the numbering wrong every time). So I implemented a command which was easy to understand. I also plan to implement a converse tactic, which dismisses goals (typically dependent existential variables), but it's not done yet.