The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/15/2016 09:51 AM, Soegtrop, Michael wrote:
> Dear Coq Users,
>
> as far as I can tell (it is not documented) eauto will execute any hint 
> first, which solves the goal, regardless of priority in the database. This 
> has the undesirable effect that eauto first checks all hints if they would 
> solve the goal, even expensive ones. I tend to give priorities to extern 
> hints such that expensive tactics are tried last, but this has no effect, if 
> all tactics are tried before any tactic is executed.
>
> I wonder how other uses see this. Do you think it is a great feature of eauto 
> or not?

It wasn't until recently in 8.5 that eauto took the hint costs into 
consideration at all - it was previously trying hints in 
most-recent-first order regardless of cost.  Yet few noticed.

-- Jonathan