The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/21/2015 03:38 PM, Jonathan Leivent wrote:
> I'm considering a way around this - it would involve using Print 
> HintDb to dump hints to a file.  Then parse the file to create a new 
> Coq script that would add the hints to a new db - but with all hints 
> for the same head symbol ("hintlets") put into a single "+" hint, like 
> so:
>
> Hint Extern 1 (_ <= _) => (apply len_n + apply le_S) : newdb.
>
> perhaps with the order of hintlets in each hint "+" tactical ordered 
> by their original cost (or order in the original db if the same cost), 
> with the overall hint cost being that of the lowest cost included 
> hintlet.
>
> I think the resulting db should fully backtrack across goals (and so 
> also be monotonic) - at least for auto, which is currently the only 
> automation tactic that can backtrack within a "+" tactical.
>
> Sound promising?  (If this sounds desperate that's because it is. ;)
>
> -- Jonathan

First obstacle : extern hints that use pattern variables or patterns 
involving more constants than just the head symbol don't print out with 
sufficient info to be parsed and re-generated.  For instance:

Hint Extern 7 (?X <> ?Y) => idtac X Y.

prints only as:

For not ->   (*external*) idtac X Y(level 7, id 0)

so, the equality (non-head constant) and binding of X and Y are all lost 
in the printout.

But, hopefully there are not many of those kind of hints - so that 
rewriting them by hand won't be too hard.

-- Jonathan