Skip to content

Resolve polymorphic drops - #733

Merged
Nadrieril merged 8 commits into
AeneasVerif:mainfrom
Nadrieril:resolve-drops
Jul 4, 2025
Merged

Resolve polymorphic drops#733
Nadrieril merged 8 commits into
AeneasVerif:mainfrom
Nadrieril:resolve-drops

Conversation

@Nadrieril

@Nadrieril Nadrieril commented Jun 13, 2025

Copy link
Copy Markdown
Member

Fixes #684. This adds an option to track drop clauses through the trait system, and generates impls that contain the drop code (either user-defined or compiler-generated, as appropriate).

Uses cryspen/hax#1543.

ci: use AeneasVerif/eurydice#232
ci: use AeneasVerif/aeneas#565

@Nadrieril
Nadrieril marked this pull request as ready for review July 3, 2025 21:58
@Nadrieril
Nadrieril added this pull request to the merge queue Jul 4, 2025
Merged via the queue into AeneasVerif:main with commit 5d2560b Jul 4, 2025
10 of 14 checks passed
@Nadrieril
Nadrieril deleted the resolve-drops branch July 4, 2025 13:26
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.

Feature request: Resolve polymorphic drop calls

1 participant