The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Taral wrote:
> On Mar 7, 2009, at 9:46 AM, "Samuel E. Moelius III" 
> <moelius AT cis.udel.edu> wrote:
>
> > 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.

You can do it with an Ltac function that uses [type of] and [assert] 
(among other ingredients).