Fix #17852 (universe issue with reverse coercions) #17853
Merged
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
coqbot-app
bot
added
the
needs: full CI
proux01
added
kind: fix
proux01
force-pushed
the
fix_rev_coerce_univ
branch
2 times, most recently
from
543979a
to
3201bd0
Compare
|
Dear @coq/universes-maintainers we would like to tag 8.18rc in 10 days. If you can review this bugfix by then I would be very happy. |
SkySkimmer
requested changes
Jul 13, 2023
There was a problem hiding this comment.
Still fails on
Record type : Type := Pack { sort :> nat -> Type }.
Definition set := fun _ : nat => Set.
Canonical UnitProp := Pack set.
Check set : type.you should use refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) on the types not some adhoc if issort then new_type hack
proux01
force-pushed
the
fix_rev_coerce_univ
branch
from
3201bd0
to
03d078f
Compare
|
Thanks both for acting quickly! |
|
Thanks @SkySkimmer it's indeed much better than my horrible hack. |
|
You should undraft and run full ci if this is ready |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
SkySkimmer
approved these changes
Jul 14, 2023
|
The windows failure seems unrelated, otherwise CI is green. |
|
@coqbot merge now |
|
@gares: You cannot merge this PR because:
|
|
@coqbot merge now |
|
It would be nice to revert the change to HB and confirm MCA has no problems |
gares
added a commit
to gares/coq
that referenced
this pull request
Jul 24, 2023
coqbot-app
bot
moved this from Request 8.18+rc1 inclusion
to Shipped in 8.18+rc1
in Coq 8.18
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.
Fixes #17852
Added changelog.(bug shouldn't appear in any released version)Added / updated documentation.Documented any new / changed user messages.Updated documented syntax by runningmake doc_gram_rsts.Opened overlay pull requests.