The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think you may be looking for bug 3199?

On Thu, Oct 15, 2015 at 7:10 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Is it the case that auto is supposed to try all (pattern applicable) hints in ascending cost order, regardless of hint declaration order?  That seems to be what the refman implies - although it says very little about cost.  However, there appear to be cases where auto will try a higher cost hint that was declared later before a lower cost hint declared earlier.  Is that a bug?

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.

-- Jonathan