[Feature request] Gate extractions to F* and ProVerif behind a single feature `hax`
Open
enhancement
- Dominant language
- F*
- Stars
- 138
- Forks
- 5
- PR merge metrics
- No merged PRs in 30d
Description
#102 and #107 both introduce features to gate extraction to ProVerif and F*, respectively. Both features are justified by an optional dependency on `hax-lib-macros` and nothing else. This suggests unifying the features into a single `hax` feature that guards any `hax` extraction specific code and dependencies.
This should also clean up redundancies in the `hax` driver.
Contributor guide
Assessment
This issue has not been assessed yet.