Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?


Chronological Thread 
  • From: Tom Prince <tom.prince AT ualberta.net>
  • To: Catalin Hritcu <catalin.hritcu AT gmail.com>, Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?
  • Date: Sat, 13 Oct 2012 17:37:36 -0600

Catalin Hritcu
<catalin.hritcu AT gmail.com>
writes:

> OK, I've simplified the test illustrating the problem even further:

There are a number of properties of databases that affect how they get
used, besides just hints. 'Print HintDb <name>.' might give some useful
information on what exactly is going on.

Tom



Archive powered by MHonArc 2.6.18.

Top of Page