coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Custom entries examples

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: coq-club AT inria.fr
Cc: Andres Erbsen <andreser AT mit.edu>
Subject: Re: [Coq-Club] Custom entries examples
Date: Wed, 31 Jul 2019 14:52:17 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT mx0a-000c2a01.pphosted.com
Ironport-phdr: 9a23:Pwxq2hbereGsPB+LpHQIab7/LSx+4OfEezUN459isYplN5qZr864bnLW6fgltlLVR4KTs6sC17OM9fG9EjVav96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMhm6twHcu8kZjYd/NKo8ywbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDMi7mrZltJ/g75aoBK5phxw3YjUYJ2ONPFjeq/RZM4WSXZdUspUUSFKH4GyYJYVD+cZIelXoJTzqVsMohWwCgeiB+3vxCFPiHLtwa06yuEhHR3G3AA8Hd8DtmnfotXvNKcVVOC41KfEwCjdYPNQ2zfy8o3IchEnofqRQ798a9fax1MuFwzblFWftZLqMz2I3ekKqGeU8/JgVeOxhG49tw5+vCOiydstionSnI4V10jE+jt/wIYzP9G3VlN0YcO9HZZWqiqUNJN2T9s/T2xnuys20KAKtJ+1cSQQ1ZgqxwPTZ+aDfoSW+h7vSeacLDRiiH54dr+zmwy+/Eiux+HmSMW51FBHpTdfnNbWrHACzRnT59CHSvRj+keh3i6C1wXc6+1YO084jLbXJ4I9zrEsiJYcq1jPEjLslEXulK+WdkIk+vO06+v5f7rqvIOTN4hxig3mM6QunNKwAfggPwQTUGWW+v6w2KDi8ED3WrlGk/07nrTDvJ3eO8gXvqu5DBVU0oYn5Ra/FTCm0NEAkHYcMF1FYBOHgJbzO17SPv/1Fuuwg1W3kDtx2vDGJqPuApPLLnTZjrjuYKt951ZGyAUv1dBf+45UCrYZLf3vXU/xrcXUAQM9Mwyp2OnqE85914MbWWKXGKCVKqLSsVmS5uIuOeaAfoEVuCyuY8QisvXplDoynUIXVaivx5oeLn6iTdp8JEDMK1DhhNUIFGYM9iF4BNTrhUeJXHQbM3y5R6Mx/Do2IImnFsHeXo2rhvqM0DrtTc4eXXxPFl3ZSSSgTI6DQfpZLXvKepY9wAxBbqCoTsoa7T/rrBXzkuc1JevPvDAAuJTlktV5+r+LzEBgxXlPF82Yllq1YSRxl2IMSSUx2fki80d80RGeyaV+hbpVGcEBvqoUADd/DobVyqlBM/63Wg/FeY3ZGlO2GtzjWWlpRYg4m4ZIe159HM6+gxyF1C2vUecY

Thanks, everyone!! (Still interested in seeing more examples, if there are
more out there… :-)

- B

> On Jul 31, 2019, at 1:41 PM, Emilio Jesús Gallego Arias
> <e AT x80.org>
> wrote:
>
> Andres Erbsen
> <andreser AT mit.edu>
> writes:
>
>> I have tried to make non-trivial used of this feature, with mixed
>> results.
>
> Yup, my feeling is that custom entries do still need some fine tuning,
> hopefully a revision will happen soon and addresss all current problems.
>
> Feedback is very welcome, but don't assume rock-solid stability yet.
>
> Kind regards,
> E.

[Coq-Club] Custom entries examples, Benjamin C. Pierce, 07/31/2019
- Re: [Coq-Club] Custom entries examples, Andres Erbsen, 07/31/2019
  - Re: [Coq-Club] Custom entries examples, Emilio Jesús Gallego Arias, 07/31/2019
    - Re: [Coq-Club] Custom entries examples, Benjamin C. Pierce, 07/31/2019