The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Yes, this is normal; eauto and autounfold and autorewrite can share database names, but use non-overlapping sets of hints in those databases.  You might want

Hint Extern 1 => unfold foo : mydb.

(Or any other number in place of 1.)

-Jason

On Fri, Jan 24, 2014 at 6:04 AM, Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com> wrote:

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