The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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