Skip to content

Conversation

andres-erbsen
Copy link
Contributor

No description provided.

@andres-erbsen
Copy link
Contributor Author

This is a simple backwards-compatible port; IMO it also makes the intent of the code cleaner. Are there objections to merging it regardless of the upstream PR?

@JasonGross JasonGross merged commit 0e14c7b into rocq-community:master Jan 4, 2025
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants