Skip to content

[Feature request] Gate extractions to F* and ProVerif behind a single feature hax #109

@jschneider-bensch

Description

@jschneider-bensch

#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.

Metadata

Metadata

Labels

enhancementNew feature or request

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions