The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

My Question: is there anyway to use tactics to build Existentials?

  I am aware of:

http://coq.inria.fr/cocorico/ExistentialVariablesInEapply

and
http://article.gmane.org/gmane.science.mathematics.logic.coq.club/5386

  My particular use case -- is that I like to use erewrite -- I specify as little as possible, put in lots of _ _'s, and have the rewrite happen. Then, later, I prove the missing terms.

  Right now, erewrite generates Existentials for me -- which I apparently can not solve using tactics and must construct the term. Is there anyway to

(1) construct existentials using tactics or

(2) have some form of rewrite generate new goals rather than existentials?

Thanks!