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

Remove unqualified universe attributes. #11663

Merged
merged 1 commit into from
Feb 25, 2020
Merged

Remove unqualified universe attributes. #11663

merged 1 commit into from
Feb 25, 2020

Conversation

Zimmi48
Copy link
Member

@Zimmi48 Zimmi48 commented Feb 23, 2020 •
edited
Loading

They were already deprecated in two major releases.

Kind: clean-up

  • Added / updated test-suite

@Zimmi48 Zimmi48 added kind: cleanup Code removal, deprecation, refactorings, etc. part: attributes #[attributes] modify the behaviour of vernac sentences. labels Feb 23, 2020
@Zimmi48 Zimmi48 added this to the 8.12+beta1 milestone Feb 23, 2020
@Zimmi48 Zimmi48 requested a review from a team as a code owner February 23, 2020 15:29
@Zimmi48
Remove unqualified universe attributes.
4f5e9b0 
They were already deprecated in two major releases.
@Zimmi48 Zimmi48 force-pushed the remove-polymorphic-unqualified branch from 0be0209 to 4f5e9b0 Compare February 23, 2020 15:33
@ejgallego ejgallego self-assigned this Feb 23, 2020
ejgallego
ejgallego approved these changes Feb 23, 2020
View reviewed changes
Copy link
Member

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, will leave a few days for comments and merge.

@ejgallego ejgallego merged commit 1528c06 into coq:master Feb 25, 2020
@Zimmi48 Zimmi48 deleted the remove-polymorphic-unqualified branch February 28, 2020 17:44
@Zimmi48 Zimmi48 mentioned this pull request Nov 4, 2020
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: attributes #[attributes] modify the behaviour of vernac sentences.
Projects
None yet
Milestone
8.12+beta1
Development

Successfully merging this pull request may close these issues.
2 participants
@Zimmi48 @ejgallego