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: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Question an 8.6 changes on typeclasses eauto (multi-goal)
Date: Thu, 10 Nov 2016 08:01:45 +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:JsUcchK0tdt6E52ZhNmcpTZWNBhigK39O0sv0rFitYgeL/rxwZ3uMQTl6Ol3ixeRBMOAuqkC07Cd6vi+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6zbL9oMBm6swrdutQKjYZjN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqJFrhy8uxxxzY3aYI+XO/p/YqzSctwUSHFdXsZIUyFNHp+wY5cRA+cHIO1Wr5P9p1wLrRamCwWiGeTvxSFHhn/qx6061PwhHRnb1wInHtIBrHTUo8/rO6cWX+y+0a7FzTDCb/xK2Tfy8pbHchQ7rfGXWrJ/b8XRyVU1FwPCllWdso3lPzWJ1usTt2iX9fZvVeWqi2M+rQx6vzahxsApiobTh4IVzEjJ9SR/wIYpO9K4TFR3bsO6H5ZWqiqUNJN2T9s/T2xspio20L0LtJ6hcCUK1pgr3R3SZv+ff4SV4x/uWvydLDl2iX5/Zr6yiRK//VK9xuD/S8W4yEtGoytBn9XWqHwA1xPe5tKZRvdn4EutxzeC2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmEX5lqCaalgo9vKp6+ThfrXpuJucO5VohQH5N6Qigs2/AeImPQgSR2WX5OCx2KP58UD5QLhGlP07nrfDvJ3ZJskXvqu5DBVU0oYn5Ra/FTCm0NEAkHkCLVJKZBKHgJL3NFHKOvz4FvC/jEqjkDd33fDGOaXhD47MLnjFjLfuY7J951RAxwo0yNBT/4hUBa0ZIPLvRk/xs8TVAQM+Mwyt2uroFNF91p4FVm+UGa+YMKbSsUeS6e41IumMYpUVuDfnJPQ/6f7ulyxxpVhIN6KuxN4cbG2yNvVgOUSQJ3T2yJ9VGmAT+wE6UebCiVuYUDcVaWzkDIwm4TRuQrmhAIjfXIe1xPSk3Sy7F5BSLCgSD1GHEX7lc8OfXPoDdDiVOudglCAJUf6qTIp3hkLmjxPz17cydrmcwSYfr5+2jNU=

Dear Jonathan,

> 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 think I would first investigate possibilities to extend the parser of Coq.
It would be nice to have something like "vernacular notations" in other cases
as well. But I think as long as version maintenance operations can be done
with regexp replace and the input is not too verbose, I think I would rather
live with it and concentrate on other topics.

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

[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