coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class)
Chronological Thread
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class)
- Date: Thu, 30 Jun 2016 22:29:38 -0400
- 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-qk0-f175.google.com
- Ironport-phdr: 9a23:/VGzhxWtVRsf2eHrIcHOaMQH3bbV8LGtZVwlr6E/grcLSJyIuqrYZheEt8tkgFKBZ4jH8fUM07OQ6PG4HzVQqsjZ+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0os2YPV0ArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7axHwaW3kWmxwAJwXE8hz8Qt+lsCz8t+lw3CSXFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==
On 06/30/2016 04:00 PM, Jonathan Leivent wrote:
...
Hint Extern 0 (eq _ _) => typeclasses eauto : tcinit_db.
Declare Implicit Tactic (eauto with nocore tcinit_db; shelve).
Yes, that could be a winner.
Although now it looks like Declare Implicit Tactic has some bugs. The declared tactic doesn't get called in all the cases it claims: "It is used every time the term argument of a tactic has one of its holes not fully resolved.". For instance, "refine _" doesn't call it.
And in one case, it is giving me: "Anomaly: Evar ?X96 was not declared. Please report."
On second thought - it seems easier to get Declare Implicit Tactic to fail than to succeed. I guess nobody uses it.
-- Jonathan
- Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class), Jonathan Leivent, 07/01/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class), Jason Gross, 07/01/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot, Jonathan Leivent, 07/01/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot, Arnaud Spiwack, 07/04/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot, Jonathan Leivent, 07/04/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot, Arnaud Spiwack, 07/04/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot, Jonathan Leivent, 07/01/2016
- Re: [Coq-Club] Declare Implicit Tactic bit-rot (was: question about Existing Class), Jason Gross, 07/01/2016
Archive powered by MHonArc 2.6.18.