The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Pierre, this command is actually documented (in a note at the bottom of the search section https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.search). It is missing an index entry though. In general, you shouldn't wonder why something isn't documented. There are never good reasons for missing documentation. So always open an issue (or even better a pull request) when you notice such shortcomings.

Michael, since 8.8 the use of deprecated notations will generate a deprecation warning. However, to be able to do this, many compatibility notations where undeprecated because their replacement was not consensual.

Théo

Le lun. 28 mai 2018 à 19:56, Pierre Courtieu <pierre.courtieu AT gmail.com> a écrit :

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.