The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Taral wrote:
> I don't think there's any way to convert an existential into a goal. 
> It sounds useful though.
>
> What I end up doing is determining the expected type of the 
> existential and creating a lemma.
That's a nice suggestion.  One could have a "Extential to goal" 
command.  This would start a fresh proof.
(all the other goals of the current proofs disappearing).  Now, there 
should exist a corresponding
"commit existential" command, that would take the proof as it is, 
consider all open subgoals as
new existentials, and instantiate with this existential.

Would that fit the need?

I read the subsequent messages by Adam on the feasibility of this task 
using LTac.  I have doubts
concerning this approach: Ltac is designed to program tactics, i.e. 
commands that work on a single goal at a time, and this is an operation 
that has an effect across the whole sequence of goals.  Now, my doubts 
maybe unwarranted, since eapply, eauto, and the like already work across 
the whole sequence of goals.

Yves