Feature Request: autoreplacing [intuition]

[JasonGross]

There is the following procedure for speeding up Coq developments and making them more robust to changes which is crying out for automation. I'm not sure if company-coq is the right level to implement the automation at, but you might know better than me.

1. Find an instance of intuition

2. Replace it with intuition debug auto with *, and execute the line

3. Take only the lines with (* success *) in the debug output

4. For each of these rules:

   a. Search the output of Print Hint * for the rule (harder with external hints, but probably doable) b. Search upwards from each occurrence to the first instance of ^In the database \(.*\):

5. Take all of the database names, sort them, and deduplicate them

6. replace intuition debug auto with * with intuition auto with <list of databases>

[jonleivent]

Nice idea. Remember to look for core and use nocore if no core hints are used!

Also, it's not just intuition - the other tactics that are implicitly "auto with *" are dintuition and firstorder.