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

[search] Add removal warning for ssr's Search #12338

Closed
ejgallego opened this issue May 16, 2020 · 0 comments · Fixed by #12341
Closed

[search] Add removal warning for ssr's Search #12338

ejgallego opened this issue May 16, 2020 · 0 comments · Fixed by #12341
Milestone
8.12+beta1

Comments

@ejgallego
Copy link
Member

#8855 removes ssr's Search from scope when ssrflect is loaded, this will be quite confusing for users, thus we should add a warning in this case to remind them to either load ssrsearch or to disable the warning if they wish to migrate.
@ejgallego ejgallego added this to the 8.12+beta1 milestone May 16, 2020
@Zimmi48 Zimmi48 self-assigned this May 16, 2020
ejgallego added a commit to ejgallego/coq that referenced this issue May 17, 2020
@ejgallego
[search] [ssr] Emit deprecated message when calling search from ssref…
dceeabd 
…lect

but ssrsearch is not loaded.

Fixes coq#12338
@ejgallego ejgallego mentioned this issue May 17, 2020
Merged
ejgallego added a commit to ejgallego/coq that referenced this issue May 17, 2020
@ejgallego
[search] [ssr] Emit deprecated message when calling search from ssref…
f076d9d 
…lect

but ssrsearch is not loaded.

Fixes coq#12338
@Zimmi48 Zimmi48 removed their assignment May 17, 2020
ejgallego added a commit to ejgallego/coq that referenced this issue May 18, 2020
@ejgallego
[search] [ssr] Emit deprecated message when calling search from ssref…
8c89cbc 
…lect

but ssrsearch is not loaded.

Fixes coq#12338
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
8.12+beta1
Development

Successfully merging a pull request may close this issue.

[search] [ssr] Emit deprecated message when calling search from ssreflect ejgallego/coq
2 participants
@Zimmi48 @ejgallego