The Coq mailing list

[Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>]

Hi,

I added some Unfold hints to a “mydb” hint database.  

Then I try “eauto with mydb.” but it doesn’t solve the goal. 

On the other hand, when I try “autounfold with mydb. eauto.” , the goal is solved.

Is this normal?   

Is there a standard way to solve such goals with a single automation tactic? Or do I really need to use two tactics (autounfold followed by eauto) ?

Best regards,

Bruno