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.
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
SSReflect's Search tool does not take Search Blacklist table into account #8663
Comments
Probably the best fix here is to remove the Search tool of SSReflect and merge whatever special features are useful in the main one. |
From the SSReflect documentation the features missing from the built-in Search are:
Of these, to me (2) is the most useful to port while the others aren't really necessary. (3) and (4) are better handled by |
Adding 2. to vanilla Coq would be easy and I can do it if noone objects. About 1., there are various syntax we could think of. For instance, we could allow We could imagine various modifiers actually, like |
Maybe no need to overthink this if actual use cases are already covered by |
SSR Search has been removed in #13760, solving this issue. |
Version
Coq 8.8.1
Operating system
macOS 10.13.6
Description of the problem
Please see the comments in the snippet below:
The text was updated successfully, but these errors were encountered: