coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Anybody uses the Quote plugin?

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Anybody uses the Quote plugin?
Date: Fri, 20 Jul 2018 09:19:49 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 7.mo177.mail-out.ovh.net
Autocrypt: addr=mail AT maximedenes.fr; prefer-encrypt=mutual; keydata= xsFNBFRYkvgBEAC0Zot4S5lKkhzYK68sSb69wVyEsugASVeWPHjVpxgFG44BLFB7Te0zWHjg jK76yCUmDdpKFdIufw5PQr+3At/8G75Y3x+dGC2rg+31fPAUJvp/AfrMloH+qd+tqxbaKjtC kymLGE01Yj8m3xaV7bN9wuYwL03+staTESJFVm3CZwNAqFgIZCG6KgBGT93ybUgbPYRrTv+n Oleags7nHdPubX6SAWbZVhuweHCwiooRBVSjzyxuhTtDuAwmeZ+ca4WE3IkOWmJmq4KbCeij HJ9B2b6qSopM19dq+iBByPu+LpBCwSA9Nr9hL1XRnoNngwf0OtJ0CNiKjKsNKlAmsCHw/o48 0IoiKP40sH+zsNFeNepbIqILPaWDvTOFvtHc9FDcH2X9NHaWx73GckMzi2z5Ty4tVoEU4Tap JlDVaKWyhvtHRwxbekgk3Vq3PcKKhcLy/xsbyknVLFw8UbFj+sYwGPrzb7j2WhpisfSct3Ii vxv2FUzM3etqM+tsJ/1Oq8u1A5lQ7lSEZmsCQdeyzMXmrUgXAEZvcx5anmTlNR3TjoG6sOxm axp9f/zgZmr9pV/FRq9tLIu8Eqv8+HqeUcHfxICcnXHVPz2x1h6H6ft45h9LGPEi1riCiZZ5 eFnq/epTkpQF411fo7sY1osaZ0Sp9yrHIPAtmJT40tmPQflSYQARAQABzSZNYXhpbWUgRMOp bsOocyA8bWF4aW1lLmRlbmVzQGlucmlhLmZyPsLBdwQTAQoAIQUCVFiS+AIbAwULCQgHAwUV CgkICwUWAgMBAAIeAQIXgAAKCRAWr2+lkXvTQPz8D/4lUpXfqOp0ZVc9WTBr8bDxHE334Bd9 FnekcYCRrmOUE76oMsK1/MhoKCEmr5bdyn8oh/r2GsNTWB1lsHpTEjYc2Sf17LNW2ncVu4OB EsD38chB9aTEev5Pc2jAA7l/WF8ceF5mkt6OjWrBfDp6yBfXwrzDfdzLixVHVyJUYA/04T7U JZc7Rjz1CdXE2wg8KL7+uq/QGc5TCPPQmlpdXJYpDgK7FtJasRoh34/pVFGHXXA1PnCe+IIL 52DynkF+bCL3sWk8A71ebUkyTO6ytqUKYafCPjrrGv4y13O+/2QcB3Iz4gDiKgvL8FWMhmhJ QF5C8BucOE87JWb5nJmq+Gs13NVofYMpmI+DDaBNJ6ns/sbR68vRfoXEhr0adPDLZOohZKJM Lu6WTjyFNNOgj1jgG0I00+tctmtW00W+U3oi36vbUXalbi5WPlIBpIXkjI9p7xoHe1mJwN40 jn/ExEXnY9uZ4H/NorJ7OzGdEOlz+ZpkcBpW34N5GZfOg7UXScA3tAFPyWcxCKsxAti0sRAR fIQXkxwt+BTBMm5m7n+wxe/2sf+xxO6AYyedWRbLaTCexJEw4Tx4+hocFT8lD6y/cGPORcak AkoWz2aiGQK07gbJ5dxymCP6g0Xcl8CloXodwV124G2++eQpucydK4BRFDTyJLJJNAR3nkei s1BBj87BTQRUWJL4ARAAqLecjPrMCx42r822nQT6e8GTHrFKwppkRqSXAucAZ4ICJ1YoT2Hy z+DtehqEV5IdIDGRivKvQYQF1Yz2NpgO7vfmB1M8ZsxyTyFeQiBkFIb5BKVhUk0xat2Xjgmb PJ59GsEbH5DCIrUqFRRGshjgul/z0adUF5DjFyuqo5TMAJdgXtJbTzmCTXoBwJmNuaUHwieK s47K9pmnnaUnkSy+CDTjtOihNeSx+lmrzieo8OyYuwvY1V1av+dJlF6YF7D5X9gHUAMsSypq pdQX0PhUZ4XheCiC0HojVzT3NEEkZ3LjuAGD7+1yaWNepGgqFqiaGEq4ihjihbvW3rCO84RS 9rSb6F7Eru7HMDUKLmUDc37GhOC0xcrTJ5zZ0CwTaM6V2P2n/FxOXEoKwRVGdAAWvh521N7k pYQpGsamfCzl8ruaEf/IhksPZiyJC95W5jXl98UDf6WNm/xKXwF60oK56iSBj+YWmUgjAzGf XRCJyiXAlMtBhErkije2iIqKVungP3N4IPEhmDOLVa9BsdXAsptkWSmWzvJA+z0A52hta0/2 B71dreoGFVnmLWWSCR+O6P9yivnfEKq75QPjBLj6xw6nXxtyhyrVT2/xOy1Osvf2mM7Gx9wR Q0Ktv7fjX2AyIrcvR3r3/RgsDA3/elqkcrY1hdu+NkOHOKtME43htXsAEQEAAcLBXwQYAQoA CQUCVFiS+AIbDAAKCRAWr2+lkXvTQNfiD/0fD2LeHa/7Vq7ClzMgjaCm5Jt2afGZi9xrD+Z8 4/wlVjFI8TZsYoiq6OTbvn6eNFE7J0wYpAouYS6GP/Ga+e/eo9Hm3BeK9+1gP0QSfwcA1+ci n+zvD5q58Movy7qo4BOoJM2eb8FpdyeloViTUlxgqocZK35ewTK0q3JcMlSZZxdOvCol3F8r CWkXqHlJoA9dL16VxBbxmT57ogqgpOFfIbc9PHMjQaNY5BWLz1+qj4bXN5UXvibP97tas1LE 4OilGPIW/ZOMItfVcxi9//huyTJt0l4lRJRochpmppItYeDs6tFyFu4XpEgUbAXwTnANqHr2 N0OSZT3j+BTMgVrs5sUgjMlqNJkMKjZmkIuSoIZbtYHfQgSY2VBPImLyWpu+XdzjBwFbuMJK 8q9tvgG2ydZCDbpC6Bi0FF+WKmZZqSkqgIFjUOkLGh624JQLbU/aezYrrhORDGEIAGtHbdn3 pC1fcAJHwI3JpRpNwou+lc8SORjUoTpSOmc5C0qWu0P7D1Y3k8gFngN/c42TX6eyyVpQw44h A6bxBs56DrE8OPyt15lveeMxT/0scd/MJlFJY/Dy+XelA0Utt0SUgSqI+TaL2eTlwNCmhNL+ ShCTVRcfb1UFlSA+GyURCLoUjrbukm7GS0pKhF+O9eCj1DkYEdi9NTjs83wKHHYu8CspWw==
Ironport-phdr: 9a23:+Lz1NBM7UeLYitvkR7Yl6mtUPXoX/o7sNwtQ0KIMzox0LfnzrarrMEGX3/hxlliBBdydt6oazbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlJiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkZNzA37WLZhMJ+g61UvB2vqAdyw5LXbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUIFeUAMudYr4zjqFAToxW5Hw+sA/r0yjRVgXL22Lc10+UlEQzd2QwvBd0PsHXRrNrrKagdT+a1w7fTzTnZYfNWwy7w5Y7VeR4vpvGMWKh/ccvXyUQ3GAPFj0mQqYz4PzyOzOgCr2+b7+9mWOmyiGAnsxl8rzeuy8s2l4XFmoIYxkrF+Clk2oo5ONK1RUpjbdOgDZdcrTyWOopqTs84Xm1lvCc3xqcbtZO6fSUHzoksyQTFZPydaYeI5wruVOaPLjd8g3JoYLCyiwy38Uin1+HxVMu53ExPriVfk9nMsmkB1xvO6sibUPd9+Vmh2TaV2wDV9O5EPVg4lavdK5E/3r49jpUevEXZEiPrhEn7jLWae0Q59uSy9ujqbbHrqoeZN4BuiwH+Nqoumta4AeQ9KgUOWnKU+eW41LD4+E32WrpLjvwzkqbHrZ/VO8IbqbCiAwNP3IYj8Q6zDy2639QAgXkHMFVFdQqbgIjuIlHCOez3DfOig1u3izpr3PDHPrj5AprXNHTDkbHhfax860FG0gYzw8pftNpoDeQKJ+u2UUvsvvTZCAU4Okq62bXJEtJ4g6YXSWOKD+e1saVSqhfc4+suJ8GJbZ8UvTvxJv4o/LjglylqyhcmYaC10M5POziDFfN8LhDBOCu+spI6CW4P+zEGYqnvgVyGXyRUYi/sDac19jA+BY6rC4rYAI630uXYgHWLW6ZOb2UDMWiiVG/yftzaCfIFeCOXL8NslDEfE7a7Gdd4iEOe8TTiwr8iFdL6vy0VsZW5iooqoejUzE5tszl9DsDY1HyRCWZqniUOSiNkhK0=
Openpgp: preference=signencrypt

Dear Coq-clubbers,

I'm trying to clean up the set of plugins shipped with Coq, so that we
can make the maintenance done by the development team more focused and
effective.

I was wondering if anybody was using the Quote plugin in real-world
developments. See https://github.com/coq/coq/pull/7894 for more context.

Thank you in advance for your feedback!

Maxime.

[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