search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

Parser.Dep: interpret inline_for_extraction on *any* decl, not just Vals #3432

Closed mtzguido closed 4 weeks ago

mtzguido commented 4 weeks ago

This is relevant for Pulse, which uses %splice to generate Vals during typechecking time, so the parser will miss the qualifier and mess up the dependency analysis.

mtzguido commented 4 weeks ago

This passed our brand spanking new check-world workflow, so I'm merging. https://github.com/FStarLang/FStar/actions/runs/10689266115