coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Is eauto behavior desirable?, (continued)
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
- RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/19/2016
- RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/20/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Matthieu Sozeau, 09/15/2016
- RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
- RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/16/2016
- RE: [Coq-Club] Is eauto behavior desirable?, Soegtrop, Michael, 09/15/2016
- Re: [Coq-Club] Is eauto behavior desirable?, Jonathan Leivent, 09/15/2016
Archive powered by MHonArc 2.6.18.