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

Fix const_relevance and default qvar handler with sort polymorphism #18340

Merged
merged 4 commits into from Nov 22, 2023
Merged

Fix const_relevance and default qvar handler with sort polymorphism #18340

merged 4 commits into from Nov 22, 2023

Conversation

SkySkimmer
Copy link
Contributor

Fix #18339

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 20, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner November 20, 2023 14:05
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 20, 2023
@SkySkimmer SkySkimmer mentioned this pull request Nov 20, 2023
Merged
@ppedrot ppedrot self-assigned this Nov 20, 2023
ppedrot
ppedrot reviewed Nov 21, 2023
View reviewed changes
kernel/cClosure.ml Outdated Show resolved Hide resolved
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 21, 2023
@SkySkimmer SkySkimmer requested review from a team as code owners November 21, 2023 16:33
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 21, 2023
@ppedrot ppedrot added the kind: fix This fixes a bug or incorrect documentation. label Nov 21, 2023
@ppedrot ppedrot added this to the 8.19+rc1 milestone Nov 21, 2023
@herbelin
Copy link
Member

Might be useful for #17950 (7d14b17), thanks!

@ppedrot
Copy link
Member

ppedrot commented Nov 22, 2023

@SkySkimmer the lean importer now needs an overlay.

@ppedrot ppedrot added the needs: overlay This is breaking external developments we track in CI. label Nov 22, 2023
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels Nov 22, 2023
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 22, 2023
@SkySkimmer
Copy link
Contributor Author

I reverted the API change instead of doing an overlay
(it was just to be able to do let create env ?(evars=of_env env) flags = ... instead of let create ?evars flags env = let evars = Option.default (of_env env) evars in ..., not worth it)

@ppedrot
Copy link
Member

ppedrot commented Nov 22, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 54e61bc into coq:master Nov 22, 2023
7 checks passed
@SkySkimmer SkySkimmer deleted the fix-sort-poly-relevance branch November 23, 2023 12:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

Anomaly "File "kernel/constr.ml", line 1483, characters 28-34: Assertion failed." with sort poly
3 participants
@SkySkimmer @herbelin @ppedrot