Skip to content

Fix --use_nbe_for_extraction option#4179

Draft
mtzguido wants to merge 1 commit into
FStarLang:masterfrom
mtzguido:nbe_extraction
Draft

Fix --use_nbe_for_extraction option#4179
mtzguido wants to merge 1 commit into
FStarLang:masterfrom
mtzguido:nbe_extraction

Conversation

@mtzguido
Copy link
Copy Markdown
Member

@mtzguido mtzguido commented Apr 8, 2026

This option was always essentially disabled since the top-level definition of extraction_norm_steps was evaluated before options were parsed, hence --use_nbe_for_extraction defaulted to false.

--

I just randomly noticed while looking at extraction normalization. I'm marking it as a draft until we add some test for it, there are none.

This option was always essentially disabled since the top-level
definition of extraction_norm_steps was evaluated before options were
parsed, hence --use_nbe_for_extraction defaulted to false.
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