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: Clément Pit--Claudel <clement.pit AT gmail.com>
To: 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:30:38 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:Egt3lha+QykHfNhOhxdRf67/LSx+4OfEezUN459isYplN5qZoMW6bnLW6fgltlLVR4KTs6sC0LuN9fi4EjVZv96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52Ihi6txndutUZjYd/N6o8ywbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRy8uRJ/zY7aboKbOvVwcazSf88VSHFOXspNTSFPBZ+wYoUPAucHIO1Wr5P9p1wLrRamGwSsAPnoyjpWiX/wwa01y/4vEQDa3AA5Bt4DrnDUo8/oNKgPT++1yLTDwDLfYPNSxzj97ZbHchY9of2WRbJwcNbRxFIgFwPAlFqQqIjlMymJ2eQKtmiW9uxtXv+hhW4grgF+uDmvxsE0h4bVgoIa0ErE9ThiwIovIN23Vkh2asOnHptIryyWKZZ6T8E4T2xqpio20KAKtJqlcCQQypkqxwbTZ+GEfoSS/B7uVfydLSliiH54Zr6yiRC/+lW6xOLmTMm7ylNKozJFktbSsnAN0ATe6s2ASvtg4ketwzWP1x3V6u5ZP080k7HbJIA7wr4uiJUTq17PETLol0nuja+WcFsr+vSw5uj5f7nrpIWQOo1qhg3kL6gjntKzDf46PwUOR2Sb/P6z1Lzn/U33WrVKifg2n7HFv5DeO8sbo7C2AwlJ0oo58xa/Dium3c8XnXkCNl1FeRaHg5L1NFHJJfD0Fe2/jEi0kDd32/DGOaXsDYnKLnjaibvuYbJ961NHxwco1tBe55dUCqkbL/7pW0/xssbYDh4jPACuzebnEoY16oRLUmWWR6SdLan6sFmS5+tpLfPfSpUSvWPWL3kg6vjyukc4hRpYVq2gwJcabDjsFfBrJkiffTz0g8spHmIDvw54R+vv3g7RGQVPbmq/CvpvrgowD5irWN/O

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.

Attachment: signature.asc
Description: OpenPGP digital signature

[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