8000 Stop using "dummy_value" in native compute by SkySkimmer · Pull Request #20704 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Stop using "dummy_value" in native compute #20704

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.

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

Merged
merged 2 commits into from
Jun 4, 2025

Conversation

SkySkimmer
Copy link
Contributor

NB: there was a comment saying "Two instances of dummy_value should
not be pointer equal, otherwise comparing them as terms would succeed"
but when I tried to assert (dummy_value () != dummy_value ()) the assertion failed...

This removes all remaining uses of dummy_value.

NB: there was a comment saying "Two instances of dummy_value should
not be pointer equal, otherwise comparing them as terms would succeed"
but when I tried to `assert (dummy_value () != dummy_value ())` the assertion failed...
@SkySkimmer SkySkimmer added this to the 9.1+rc1 milestone Jun 3, 2025
@SkySkimmer SkySkimmer requested review from a team as code owners June 3, 2025 14:49
@SkySkimmer SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. request: full CI Use this label when you want your next push to trigger a full CI. labels Jun 3, 2025
@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 Jun 3, 2025
@ppedrot ppedrot self-assigned this Jun 3, 2025
@ppedrot
Copy link
Member
ppedrot commented Jun 4, 2025

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 6c274d1 into rocq-prover:master Jun 4, 2025
7 checks passed
@SkySkimmer SkySkimmer deleted the native-dummy branch June 4, 2025 12:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants
0