Skip to content

Commitments: give interface file and OCaml wrapper

Antonio Locascio requested to merge alocascio@fstar-module-extraction into master

Related #16

The goal of this MR is to move the Commitments module to the interface file [Commitments.fsti]. Additionally, we define an OCaml wrapper [Commitments.ml] to be able to run the extracted code.

  • Move Commitments module to fsti
  • Define OCaml wrapper
  • Add Makefile rule to build extracted code

Reviewers: @paracetamolo and @germanD

Edited by Antonio Locascio

Merge request reports