The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le vendredi 13 février 2015, Jonathan Leivent <jonikelee AT gmail.com> a écrit :
> 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 ;)

Indeed that's pushing it :) I suspect you'll get the same performance with has_evars, and it could be the case that abstract will work in presence of evars someday.

Best,

-- Matthieu  

--