Skip to content

Use promoted MIR by default#671

Merged
Nadrieril merged 1 commit into
AeneasVerif:mainfrom
Nadrieril:promoted-by-default
Nov 12, 2025
Merged

Use promoted MIR by default#671
Nadrieril merged 1 commit into
AeneasVerif:mainfrom
Nadrieril:promoted-by-default

Conversation

@Nadrieril
Copy link
Copy Markdown
Member

@Nadrieril Nadrieril commented Apr 29, 2025

Second attempt at #605 (reverted in #614) now that we handle unevaluated promoted constants (#669).

ci: use AeneasVerif/eurydice#336

@Nadrieril Nadrieril changed the title Promoted by default Use promoted MIR by default Apr 29, 2025
@Nadrieril Nadrieril marked this pull request as draft April 29, 2025 14:50
@Nadrieril Nadrieril force-pushed the promoted-by-default branch 2 times, most recently from d353c59 to 768b71f Compare May 5, 2025 14:03
@Nadrieril Nadrieril force-pushed the promoted-by-default branch from 768b71f to 73e07eb Compare June 4, 2025 15:34
@Nadrieril Nadrieril marked this pull request as ready for review June 4, 2025 15:35
@Nadrieril Nadrieril marked this pull request as draft June 13, 2025 15:58
@Nadrieril Nadrieril marked this pull request as ready for review November 12, 2025 15:16
@Nadrieril Nadrieril enabled auto-merge November 12, 2025 15:19
@Nadrieril Nadrieril added this pull request to the merge queue Nov 12, 2025
Merged via the queue into AeneasVerif:main with commit d940684 Nov 12, 2025
11 of 12 checks passed
@Nadrieril Nadrieril deleted the promoted-by-default branch November 12, 2025 15:21
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