Skip to content

Remove unit_metadata hack#1127

Merged
Nadrieril merged 3 commits intoAeneasVerif:mainfrom
Nadrieril:remove-unit-metadata
May 7, 2026
Merged

Remove unit_metadata hack#1127
Nadrieril merged 3 commits intoAeneasVerif:mainfrom
Nadrieril:remove-unit-metadata

Conversation

@Nadrieril
Copy link
Copy Markdown
Member

@Nadrieril Nadrieril commented May 7, 2026

This hack was added because back then aeneas didn't support some ConstantExprKind variants and it felt cleaner not to expand that. Time has taught me that this was a mistake.

ci: use AeneasVerif/eurydice#402
ci: use AeneasVerif/aeneas#985

Nadrieril added 2 commits May 7, 2026 10:15
All this to avoid adding a variant in the output of
`simplify_constants`... Not worth it.
@Nadrieril Nadrieril force-pushed the remove-unit-metadata branch from 4bc42e4 to 769431f Compare May 7, 2026 08:42
@Nadrieril Nadrieril enabled auto-merge May 7, 2026 08:42
@Nadrieril Nadrieril added this pull request to the merge queue May 7, 2026
Merged via the queue into AeneasVerif:main with commit 041dc4a May 7, 2026
5 checks passed
@Nadrieril Nadrieril deleted the remove-unit-metadata branch May 7, 2026 09:27
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.

1 participant