Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] backtracking issue with typeclasses eauto

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] backtracking issue with typeclasses eauto


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] backtracking issue with typeclasses eauto
  • Date: Mon, 7 Mar 2016 16:45:25 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f48.google.com
  • Ironport-phdr: 9a23:8uPm0xUT+rAkYQ7e3pHoal61B6zV8LGtZVwlr6E/grcLSJyIuqrYZhCGt8tkgFKBZ4jH8fUM07OQ6PC/HzxZqs/d4DgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2MJVURz2PhMftbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09qBA7M8BHzWN/Vvyrku+xhkH2YOsv3Tr0wVDmK4KJiSRuugyACYW1quFrLg9B92foI6CmqoAZyltbZ


On 03/07/2016 04:37 PM, Matthieu Sozeau wrote:
... Moving
typeclasses eauto (along with auto ...) to the new engine is part of
my current plans. This should bring Hint Externs with multiple
successes as well.



+1.

IIRC, one problem with auto (the current best at backtracking) is that one cannot backtrack back into a successful auto - in other words, it acts like a big match instead of a big multimatch. Hence if "the new engine" is the one that auto currently uses in 8.5, that should perhaps also be fixed.

-- Jonathan


Archive powered by MHonArc 2.6.18.

Top of Page