coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is there a way to hide deprecated lemmas in Search?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Is there a way to hide deprecated lemmas in Search?
Date: Sun, 27 May 2018 08:42:51 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.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 mga04.intel.com
Ironport-phdr: 9a23:IvCEqxDs9k/zYAnWc3/MUyQJP3N1i/DPJgcQr6AfoPdwSPT/pcbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xboQ6uqBNkzoHOfI2YMOBzcr/Bcd8EQ2dKQ8ZfVzZGAoO5d4YDAfcPPeFGoInyu1sOtxy+BRG0COjyzTFIh2P53a0g3Os/FQHK0hErEtULsHTVsNr1NL0dXv6xzKXS1jXDaO1Z2Tjh6IjSdRAhueqBXbN2ccrN10YvExnJgUmXqYzgJj6Y0PkGvWac7+plT+2vimgnphlwojip2scjlI3JipgIxV/a8yhy3YU7JcWgRUJmZdOoDoFcuiGaOodsQs4uXXtktDskxrEaoZK3YSkHxZo9yxPRZfGLaZaE7xznWeqLPDt1h25pdKqiixuz9UWs0PPwW8m73VpQsCZJiMTAu3MP2hHV98OJUOFy/l271jaKzw3T6v9LIUQzlafDLp4hzaQ/moYcvEjZHy/2nln2g7GSdkk+5ueo7OHnbq3npp+aKYB0lhnzPrkql8ChG+g1MggDU3Kb9OiizrHv4FP1TKlSgv0ziKbZsZTaJcoBpq6+Bg9YyoMj6xejADemytsXg30HIEheeBKAkYfpNE3OIOr/DfenmFmskTFrx+zYMb3lGJnCMn/DkLL5cbZn90Fc0BYzzcxY559MFr4BJ+vzVlbtu9zcEx82KBe5w/3nCdV4zoMRQ3iDAq6fMKPIsF+H/PgjI+eWZNxdhDGoYfMi/rvliWIzsV4bZ6igm5UNIjjsFfN/Zk6dfHDEg9EbEG5MsBBoH8Lwj1jXGwVUanmuRaUkonkeCYmmBIrHDMj5hb2K3C62GttNYW1JFkqLCV/pcZmJX7EHbyfEcZwpqSANSbX0E9xp7hqprgKvk+M2fNqRwTURsNfY7PYw4uTSkR8o8jktVpac1X2ASyd/mWZaHmZqjpA6mlR0zxK46YY9m+ZRTIUB5vVVXwN8PpnZnbQjVoLCHznZd9LMc26IB9WrBTZoEYA0zNZWPwB8HcmvilbI2C/4W7I=

Dear Coq Users/Team,

I wonder if there is an option to disable listing deprecated lemmas in Search. Many lemmas have several names, a current name and a deprecated name. I can usually tell which is which, but it doesn’t make searching easier to have everything listed a few times.

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] Is there a way to hide deprecated lemmas in Search?, Soegtrop, Michael, 05/27/2018
- Re: [Coq-Club] Is there a way to hide deprecated lemmas in Search?, Pierre Courtieu, 05/28/2018