The Coq mailing list

[Taral <taralx AT gmail.com>]

On Mar 7, 2009, at 9:46 AM, "Samuel E. Moelius III" <moelius AT cis.udel.edu 
> wrote:
> (I hope this isn't a stupid question...)

No. I have the same one.

> If I have an uninstantiated existential variable, is there a way to  
> supply it interactively, as opposed to supplying it all-in-one-go  
> via instantiate or Existential?

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.

--
Taral