coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Is there a way to hide deprecated lemmas in Search?
- Date: Mon, 28 May 2018 19:55:31 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot0-f180.google.com
- Ironport-phdr: 9a23:1P9bdhAhuRJCyVTdvbgaUyQJP3N1i/DPJgcQr6AfoPdwSPvzpsbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsleVyJDDY28YYUBDPcPM/hEoITmu1sCsQGzCRWwCO/zyDJFgGL9060g0+QmFAHLxBYuH9MQv3TOttX6KroZXP6yzKnV1zXDc/JW1ing6IPVdR0hufCMUqxqccrL10YjDR/KjlKNqYz/IzOV1/oCs3WA4upvUOKgkW8nqwVrrjezwccsj5DEi4QIwV7H7SV02IQ4KNKiREJmf9KpEIFcuiKEO4dsX88vQH1ktSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wrmVOmLIDd4gGtpeLWjhxqu6ESgxPDwW8qo3FpQoSpFld7Mtn8J1xPN8MSIVvx9/kK51TaO0QDc9P1ELFg2mKfUMZIt36A8m5oJvUnAACP6glj6gayKekk8/+in8eXnYrHopp+GMI90jxnzMrwvmsOhG+Q4KBYBU3KH9uS7yb3j51H5QLRUgf0riaTZv5XaKt4apq69GQNazoEj6xOnAze8zNsYhWUHLE5CeB+fk4fpPEjOLOnkAve7nlSjiyxmx+vGP73kGpXCNGLPkLbnfbZn6k5T0hA/zd5F58EcNrZUC/XqEmT1qdaQWhQ+Kkm/x/vtINR7zIIXH2yVVPy3KqTX5GeJ6/g1LqGnY5IPpDfwNrBx///jl2U031QaYLO13JYKQH+9F/ViZU6eZCy/0Z86DW4Ws19mH6TRg1qYXGsWPi7qBvNu1nQAEIujSLz7aMWoib2F0j28G8QPNG9DA1GIV3zvctfdAqteWGepOsZk1wc8e/25UYZ4jEOhsQb7z/xsKe+GonRF56Km78B84qjorT939TFwCJ7DgWSETmUxmX9QAjFvjPg5rkt6xVOOl6N/hq4AGA==
Hi Michael,
Apart from exclusion mechanism coming with the Search command itslef:
Search foo -bar -"string" ... outside Bar.
There is a blacklisting mechanism (undocumented, I don't know why). But it
only supports string exclusion AFAIK:
Add Search Blacklist "foo".
Will exclude any ident containing "foo" in its name from the results of
Search (in PG: M-x coq-search-blacklist-stringset or menu
"coq/setting/search Blacklist" in PG).
All this does not really answer your question but you may be able to remove
the most annoying answers from Search using these.
P.
- [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
Archive powered by MHonArc 2.6.18.