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

Remove unused Nativevalues.arrayinit and arraymap #16575

Merged
merged 1 commit into from
Oct 3, 2022
Merged

Remove unused Nativevalues.arrayinit and arraymap #16575

merged 1 commit into from
Oct 3, 2022

Conversation

SkySkimmer
Copy link
Contributor

No description provided.

@SkySkimmer SkySkimmer requested a review from a team as a code owner September 29, 2022 14:49
@SkySkimmer SkySkimmer mentioned this pull request Sep 29, 2022
Merged
@ppedrot ppedrot self-assigned this Sep 29, 2022
@ppedrot ppedrot added the kind: cleanup Code removal, deprecation, refactorings, etc. label Oct 3, 2022
@ppedrot ppedrot added this to the 8.17+rc1 milestone Oct 3, 2022
@ppedrot
Copy link
Member

ppedrot commented Oct 3, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 6fbfc3e into coq:master Oct 3, 2022
@SkySkimmer SkySkimmer deleted the unused-array-nativeval branch October 3, 2022 10:58
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: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Milestone
8.17+rc1
Development

Successfully merging this pull request may close these issues.
2 participants
@SkySkimmer @ppedrot