The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/13/2015 11:36 AM, Soegtrop, Michael wrote:
> ... Your Ltac script is easily extended to this, but I wonder how efficient 
> it is, when applied repeatedly in some automation script.

Sorry I forgot to respond to this:  You can use "has_evar" to perhaps 
make the tactic more efficient by avoiding the context searches unless 
an evar is present (assuming that has_evar does the searches faster 
internally, of course).  However, note that "has_evar" will succeed even 
when the only evars present are under binders - at which point context 
won't find them.

There is also a surprisingly simple but extremely kludgey way to 
determine if there are any evars anywhere in a goal without searching 
via has_evars or context - but again it will succeed even if the only 
evars are under bindiers.  It relies on the fact that the abstract 
tactic fails if there are any evars present:

Ltac has_evars_somewhere := try abstract fail 1 "no evars present".

I haven't measured the performance of this relative to using has_evars 
on every hypothesis and the conclusion.  I also suspect that several Coq 
developers might have become nauseous by seeing that tactic ;)

-- Jonathan