coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Custom entries examples

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Andres Erbsen <andreser AT mit.edu>
Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Custom entries examples
Date: Wed, 31 Jul 2019 19:41:40 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:EuggMRJhoW+iTHXCfNmcpTZWNBhigK39O0sv0rFitYgRL/TxwZ3uMQTl6Ol3ixeRBMOHsqgC2red6vm7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCejbb9oKBi7rQrdutQLjYZsN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhTwZPDAl7m7Yls1wjLpaoB2/oRx/35XUa5yROPZnY6/RYc8WSW9HU81MVSJOH5m8YpMPAeQfIOhYqIf9qVUMohW9CwajC//gxyRUhnPqx6A2z/gtHBvE0QEmAtkAsG7UrNLwNKoKXu61yajIzTHCb/NRwTjz7JbHcgs7ufGXRb1+cNDeyU0rFwzbgVWQrpTqMi+P1uQMqWeb9PdrWOWxhGM8pAB8oSSjyt0rionTiYIY01bJ/jh6zoYtPdC0VU12bN2+HJdOqS2XNpF6Tt4gTm11oio217MLtYCjcCUIypkr3QPTZvKGfoSS/x7uUOScLS1liH9reb+ygQu5/1K6xe3mTMa01U5HripbndnIsXAAzxPS58ubRvdn+UehwzmP2xjS6uFCP080ibLWJ4Miz7MzjJYfr1rPEy7slEnrjqKaa18o9vWm5uj5ernmo4WTN45wigHwKKQuncm/DPwmPQUVUGmW+viw2Kfk/U3jT7VGluc2nbXBsJDGOcQboba0DBNS0oY68hqwEzOm0MkDknQcN1JEeBeHj5DzNF3UIfD4C+2/g1W2nztxyfDGJO6pPpKYB37Pirr6NZtn4VVRzkJnxNZT/Z9PB6spJfPvHEL9qYqLIAU+NlmZxufjCdJK9I4Fy3m4LaadNK7dtmih/OMmOKHYaacF6G67LOIqsa29xUQlkEMQKPH6laAcb2q1S7E/ex3APSjcx+wZGGJPhTIQCfTwgQzQQW4LIXGoUPBkv2xpOMedFY7GA7uVrvmB0SO8T89GNjgADUqDQy6xJte0HswUYSfXGfdP1zkNVLyvUYgkhEO+5Fe8zKBofLPZ
Organization: X80 Heavy Industries

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