pr 1390 cherry picked #1430
Merged
pr 1390 cherry picked #1430
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Closed
This is incorrect, and it was causing incoherency (inferred equiv between named classes)
|
I'm fine with merging this and editing from there. There's some more to refactor at the top and mid level as a result of the change, but we can do this in subsequent PRs |
wdduncan
approved these changes
Aug 30, 2023
pbuttigieg
approved these changes
Aug 30, 2023
|
Thanks! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR replaces #1390, which itself was a continuation off #1251
1390 was difficult to salvage as it contained many changes and was a continuation off of a PR that was itself almost two years old, it also merged in master rather than rebasing or ff-merging. I cherry picked the 3 commits, and resolved the two conflicts that had arisen.
I also made one change of my own - I removed an axiom "lake composed-primarily-of some seawater"
The commit record should record the provenance of all changes in this PR