Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ssr] Search Blacklist does not work #9061

Closed
CohenCyril opened this issue Nov 23, 2018 · 1 comment
Closed

[ssr] Search Blacklist does not work #9061

CohenCyril opened this issue Nov 23, 2018 · 1 comment
Labels
resolved: duplicate(d) Closed in favor of another issue about the same bug.

Comments

@CohenCyril
Copy link
Contributor

CohenCyril commented Nov 23, 2018 •
edited

Version

The Coq Proof Assistant, version 8.8.2 (November 2018)
compiled on Nov 4 2018 11:41:44 with OCaml 4.06.1

Operating system

Linux [...] 4.14.79 [...]-NixOS SMP Sun Nov 4 13:52:51 UTC 2018 x86_64 GNU/Linux

Description of the problem

The following script

Require Import ssreflect.
Add Search Blacklist "or".
Search or.

does not filter out lemmas whose name contain "or", while it works for coq "normal" Search https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html?highlight=search#coq:table.search-blacklist-string

Side note: it was not obvious to me from the doc of coq that the commands are Add Search Blacklist string and Remove Search Blacklist string and not Search Blacklist string.
@CohenCyril CohenCyril changed the title Search Blacklist non conform with its documentation [ss] Search Blacklist does not work Nov 23, 2018
@CohenCyril CohenCyril changed the title [ss] Search Blacklist does not work [ssr] Search Blacklist does not work Nov 23, 2018
@maximedenes
Copy link
Member

AFAICT, this is a duplicate of #8663.

@Zimmi48 Zimmi48 added the resolved: duplicate(d) Closed in favor of another issue about the same bug. label Nov 29, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
resolved: duplicate(d) Closed in favor of another issue about the same bug.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@CohenCyril @maximedenes @Zimmi48