Skip to content

fixes #1437, supersedes #1836 #1916

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
Merged
merged 2 commits into from
Feb 3, 2023
Merged

fixes #1437, supersedes #1836 #1916

merged 2 commits into from
Feb 3, 2023

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Jan 25, 2023 •
edited by MatthewDaggitt
Loading

Fixes #1437

@jamesmckinna jamesmckinna mentioned this pull request Jan 25, 2023
Closed
@MatthewDaggitt MatthewDaggitt added this to the v2.0 milestone Jan 26, 2023
@MatthewDaggitt
Copy link
Contributor

Thanks! Looks good apart from a CHANGELOG entry needed!

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Jan 26, 2023 •
edited
Loading

Ah... I think as I wasn't changing any actual proofs, only their internal names, that no entry was required. Which section do such things belong in (there is no deprecation, as such, and I've certainly added no warnings to that effect)
EDITED: I've added a paragraph (lines 680--694) to CHANGELOG hopefully it fits the bill. Maybe the CHANGELOG should also include a "Breaking changes" section?

@MatthewDaggitt
Copy link
Contributor

Maybe the CHANGELOG should also include a "Breaking changes" section?

Everything in the first section is a breaking change 🤷

@MatthewDaggitt MatthewDaggitt merged commit 833f0fa into agda:master Feb 3, 2023
@jamesmckinna jamesmckinna deleted the issue1437 branch February 3, 2023 13:24
@andreasabel andreasabel mentioned this pull request Jul 24, 2023
Merged
@andreasabel andreasabel mentioned this pull request Aug 27, 2023
Merged
@jamesmckinna jamesmckinna mentioned this pull request Oct 1, 2023
Merged
2 tasks
@andreasabel andreasabel mentioned this pull request Oct 12, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
breaking bug naming
Projects
None yet
Milestone
v2.0
Development

Successfully merging this pull request may close these issues.

Fix equality combinator names in Data.Rational.Unnormalised.Properties.≤-Reasoning
2 participants
@jamesmckinna @MatthewDaggitt