Skip to content

Various changes to compile new files in coq

Guillaume Claret requested to merge guillaume-claret@various-changes-to-compile-new-files-in-coq into proto-proposal

Reopening of !245 (merged)

We make various changes to compile new files in Coq with coq-of-ocaml. In particular, we:

  • add some axiom annotations for functions using GADTs;
  • remove the mutual dependency of definitions which are not actual mutual;
  • annotate some function types so that they are not polymorphic where it is not expected.

Part of a larger goal to compile the protocol in Coq.

Merge request reports