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

add test for elaboration of reverse coercions #17527

Closed
wants to merge 1 commit into from
Closed

add test for elaboration of reverse coercions #17527

wants to merge 1 commit into from

Conversation

andres-erbsen
Copy link
Contributor

@andres-erbsen andres-erbsen commented Apr 26, 2023 •
edited

@andres-erbsen andres-erbsen added part: coercions The coercion mechanism. part: test-suite The testing suite. labels Apr 26, 2023
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 26, 2023
@andres-erbsen andres-erbsen removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 26, 2023
@SkySkimmer SkySkimmer requested a review from a team April 26, 2023 11:29
@proux01
Copy link
Contributor

proux01 commented Apr 28, 2023

As noted in #17484 we may not want that.

@ppedrot
Copy link
Member

ppedrot commented Nov 16, 2023

IIUC this can be closed.

@ppedrot ppedrot closed this Nov 16, 2023
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
part: coercions The coercion mechanism. part: test-suite The testing suite.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@andres-erbsen @proux01 @ppedrot