The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jacques Garrigue wrote:
> I really wish there were a version of rewrite that would not
> match on existentials.
>   

I'm with you on this one, and I know Matthieu Sozeau is aware of the 
problem and will probably address it somehow in a future Coq release.

> Alternatively, is there any way to detect whether the current goal
> contains existentials? I've written a tactic to do that, but it seems
> rather ad-hoc (it just tries to instantiate, and fails when succeeding).
>   

Not the the following leads to a more elegant solution, but it may be 
useful: I've found that existentials are the only terms that don't match 
against themselves.  That is, here is code to test if a term is an 
existential:

Ltac isNotEx e := match e with e => idtac end.