Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Is eauto behavior desirable?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Is eauto behavior desirable?


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] Is eauto behavior desirable?
  • Date: Fri, 16 Sep 2016 08:10:47 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga01.intel.com
  • Ironport-phdr: 9a23:RsYA+BLDcyvH+r7t6tmcpTZWNBhigK39O0sv0rFitYgUKvvxwZ3uMQTl6Ol3ixeRBMOAuqsC1LSd6vqwESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJH93OervpbXfg9ghTynYLo0Ig/85VHasdBTio9/II4wzAHIqz1GYbIF63lvIAfZpBHx6duq+4YnuwFRsPIo+soKGfH/fq84RLFcSi8hPm8p/srznRjFUQaLoHAbVzNFwVJzHwHZ4USiDd/KuSzgu78l1Q==

Dear Jonathan,

> It's not just bad for performance. There are occasions where one has
> multiple subgoals with evar interdependencies such that one cannot accept
> just any arbitrary solution to one of the subgoals, as that solution might
> prevent solutions in the other(s).

Indeed, I have cases where some tactic creates a special hint hypothesis
which enables other tactics, so that I make sure that the second tactic
doesn't run before the first one. It would be easier if eauto would stick to
the priorities given.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928




Archive powered by MHonArc 2.6.18.

Top of Page