Skip to content

Improve the extraction to OCaml

Guillaume Claret requested to merge test-extraction into master

With this MR we improve the extraction from Coq to OCaml by:

  • having all the OCaml functions translated to Coq;
  • having a computable version of the extensible types;
  • having a try-with which could be extractible;
  • having a definition for the sets and maps.
Edited by Guillaume Claret

Merge request reports