coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] eauto with unfold hints, Bruno Woltzenlogel Paleo, 01/24/2014
- Re: [Coq-Club] eauto with unfold hints, Jason Gross, 01/24/2014
Archive powered by MHonArc 2.6.18.