The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 10/15/2015 07:10 PM, Jonathan Leivent wrote:
> ...
>
> Interestingly, it looks like using auto with nocore and a small db can 
> outperform combining the hints from that small db into a single 
> recursive match-based tactic.  However, I'm finding it difficult to 
> use hint cost to control the order in which hints are tried.

Some more about this:  The cost-vs-order for hints bug (3199) has been 
fixed in the latest 8.5 builds, but the performance advantage of [auto 
with nocore mydb] with a set of Extern hints in mydb still exists over a 
recursive Ltac tactic where each of those "hints" is a branch of a 
single match construct.  In one case I have, its 464 seconds vs. 579 
seconds - about a 20% improvement.

Of course, there are limitations to using auto as a replacement for 
recursive match - the obvious one being that auto must either solve all 
goals or leave them unchanged.

-- Jonathan