Skip to Content.
Sympa Menu

coq-club - [Coq-Club] eauto with unfold hints

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] eauto with unfold hints


Chronological Thread 
  • From: Bruno Woltzenlogel Paleo <bruno.wp AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] eauto with unfold hints
  • Date: Fri, 24 Jan 2014 15:04:42 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page