coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Anybody uses the Quote plugin?

From: "John Wiegley" <johnw AT newartisans.com>
To: Tej Chajed <tchajed AT mit.edu>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Anybody uses the Quote plugin?
Date: Fri, 20 Jul 2018 11:45:32 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=johnw AT newartisans.com; spf=Pass smtp.mailfrom=johnw AT newartisans.com; spf=None smtp.helo=postmaster AT wout5-smtp.messagingengine.com
Ironport-phdr: 9a23:Jl8XcBJ4MJTRv35iXdmcpTZWNBhigK39O0sv0rFitYgeL/zxwZ3uMQTl6Ol3ixeRBMOHs6wC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwRFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJBUMhPSiJOAI2yb4wMAeoPM+lXoJXyqkASrReiHwSgGP/jxyVUinLwwKY00/4hEQbD3AE4Ed4AtHPUrNXzNKwPUe+1zbfHzTrHb/xI2Tbx5pXDfxcjofGLXbJwd8TQxFIpFwzbgFSfs5blPy+U1uQWqWeb6fFgWfizhG4grgF8uz6izdoihInOg4Ia0FHE9SNhzYYzO9K5RlR0YcS4EJtRrCGVLY12Qtg4T250vyY6z7sLsoO4cigS0JkqxhHSZ+aaf4WH4B/vTvudLSl2iX5/Zr6zmg6+/Eqhx+HmSMW53llHojBEn9TIrHwByhPe58yBR/Bg5EmuwyyP2BrW6uxcIUA7i67bK5k5z78+kZoTrFjDEy/vlEXtia+Wal0k9vKt6+v5ebXmvYWTN4B1igH4PaQhhMq/Aes5MggIQWeX4/iz1Lrm/UHhQbVKiOM5krXBvZ3bKskXvLO1DgBX34o59hqzETmr3M4GkXUaNF5FfQiIj4ntO1HAOvD4CvK/jkyukDdsx/DGOLPgD47LLnfdnrbuZ6x961JdyAoo199f4YlUBqsdL/L0X0/9rMbYAQMhMwyo3+bnD81w2Z8ZWWKWG6OWLKfSsUKT6e80OOmNZIoVuC7nJPQ/5v7ui2U5mV4HcqWz05sXciPwIvMzH0ibKVHsi9UMHS9eogE+Re7nhHWHUCIVanqvCfES/DY+XciECofFDr+sjbOF0TbxVslUYWBAFXiKHGjhbZmFQP4Kc2SZJco3wW9MbqSoV4J0jULmjwT90bcya7OMonRJ56Km78B84qjorT938DV1C8qH1GTUEDNyk3wBXSM3x6l5ugp2zVLRiPEk0cwdLsRa4rZyail/LYTVlrMoDd3tUxjdf8yATk3gSdKjU2loE4ABhuQWakM4IO2MyxDO2y3xWe0KkKGXWdkv977EmX38PN10xHfA26QngFggT41EMmj03qM=
Organization: New Artisans LLC

I would also support dropping Quote; each time I've been able to use it, I
ended up just copying Ltac macros from existing templates so I would have the
configurability needed for future changes.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Anybody uses the Quote plugin?, Maxime Dénès, 07/20/2018
- Re: [Coq-Club] Anybody uses the Quote plugin?, Tej Chajed, 07/20/2018
  - Re: [Coq-Club] Anybody uses the Quote plugin?, John Wiegley, 07/20/2018
  - Re: [Coq-Club] Anybody uses the Quote plugin?, Hugo Herbelin, 07/22/2018
    - Re: [Coq-Club] Anybody uses the Quote plugin?, Matthieu Sozeau, 07/23/2018
      - Re: [Coq-Club] Anybody uses the Quote plugin?, Jason Gross, 07/27/2018
    - Re: [Coq-Club] Anybody uses the Quote plugin?, Christian Doczkal, 07/31/2018