The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Can one transform an existing evar into such a thing?  Or only those introduced by refine?

 I don't have a good method to transform otherwise introduced existential variables into goals at the moment. Either they were introduced by a refine, or you can use the Grab Existential Variables command when no goal is left to turn all the remaining existential variables into goals.