The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Samuel E. Moelius III 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?

You can use the [evar] tactic to create new existentials, and then you 
can use [instantiate] to replace the old existential with a term that 
uses the new existentials.  This doesn't tend to work out very smoothly, 
and generally it is a sign of a proof design flaw if you find yourself 
wanting to instantiate existentials explicitly.  Good automation with 
[eauto] and friends tends to stamp out such troubles.