Skip to content

Add some coq-of-ocaml attributes and minor changes

Guillaume Claret requested to merge guillaume-claret@coq-of-ocaml-attributes-and-minor-changes into proto-proposal

Reopening of !250 (merged)

We add some code attributes to help coq-of-ocaml, mostly coq_axiom attributes to ignore some definitions using GADTs. We also rename the Log constructor to LogElement to prevent collision with the Log module name.

Context

This merge request should help to compile the protocol to Coq with coq-of-ocaml. Part of the task https://gitlab.com/nomadic-labs/tezos/-/issues/199 to compile the Michelson interpreter in Coq. Generated Coq visible here.

Manually testing the MR / Automatic testing

This MR should not change the behavior of the protocol.

Merge request reports