coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal)

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal)
Date: Wed, 9 Nov 2016 16:48:17 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f193.google.com
Ironport-phdr: 9a23:EDGg6hF0kkhpDkkKceqc/J1GYnF86YWxBRYc798ds5kLTJ78oM2wAkXT6L1XgUPTWs2DsrQf2rGQ6/irADVeqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLd8IRmssQndqsYajZZ/Jqsw1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrxCvpxJ/zYDaY5ybOuRica3SZt4aWXNBU9xNWyBdHo+xbY0CBPcBM+ZCqIn9okMDoRWkCwa2GePvziJDi2Ps0aYnzuohDR/J0xAjH9IKrnvUttv5P7oVXOCu0KnH0ynMb/BN1Dfm9IjHbAwuofKXXbJ3f8rR1VMjGB/CjlWVsIHoOS6e2OoKs2ie9eVgVOSvhnY7pAF1uDev3NosipLTioIQ1F/J8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN4uTmNytConzrALt5i2dzUQxps93R7QcfmHfpCI4h39UOaRJi91hHd/d7K+gxa+6FWgxffgWsWt3lZGsy5In9fWunAC0BzT7ceHSv9j8Uu7xTmP0AXT5vlFIUAyi6XbN4YszqAsmpcXq0jOHS/7lF/ogKOLdEgo4PWk5uDpb7n+o5+TLY50igXwMqQ0ncy/BPw1MhMSX2eF5eu816bj/Ur3QLVWlfA2nazZv4rbJcQfvKK2HwhV0oM75xalEzimyMgYnWUALF9dZB2HiJHpN0jSL/D8EPewmE+hkCxrxvDDJr3uGI/BLnnFkLf7fLZy8VRQyAQpzYMX25UBAbYYZfn3R0W54NffF1oyNxG+6+fhEtR0kI0EDzGhGKicZenquEKMrstpa9KQaYQWvDvnYbBx/OLjhnwRgkMQdqqy2pULLnu/G6I1cA2ifXPwj4JZQi8xtQ0kQbmyhQ==

This nice trick can probably be made to work with the forthcoming
PG/xml with a small change.

-- Paul

On Wed, Nov 9, 2016 at 4:30 PM, Clément Pit--Claudel
<clement.pit AT gmail.com>
wrote:
> On 2016-11-09 16:05, Jonathan Leivent wrote:
>>
>> On 11/09/2016 11:43 AM, Soegtrop, Michael wrote:
>>> Dear Jonathan,
>>>
>>> thanks for pointing out the Tactic Notation trick! I give it a try.
>>> I would make sure that I do this in a way so that I can use sed to
>>> change to whatever other mechanism for this is supported in future
>>> versions of Coq.
>>
>> Would you consider running the Coq scripts through a macro
>> preprocessor, so that those ugly foo/bar redefinitions can be
>> abstracted into a macro?
>>
>> I recall once asking someone whether there was a way to place a macro
>> preprocessor between coqtop and its IDE (PG in my case), but I don't
>> recall the answer...
>
> See my comment on
> http://coq-blog.clarus.me/why-and-how-to-write-code-compatible-with-many-coq-versions.html
> (maybe?)
>
> Cheers,
> Clément.
>

[Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/09/2016
- Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
  - RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/09/2016
    - Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
      - Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Clément Pit--Claudel, 11/09/2016
        
        Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Jonathan Leivent, 11/09/2016
        
        Re: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Paul A. Steckler, 11/09/2016
      - RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal), Soegtrop, Michael, 11/10/2016