The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

(I hope this isn't a stupid question...)

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?

Also, just out of curiosity, why are instantiate and Existential two 
different tactics?  Is this somehow easier to implement?

Sam