Skip to content

Compile `block_header_repr.ml` and `michelson_v1_primitives.ml` in Coq

Guillaume Claret requested to merge guillaume-claret@block_header_repr-and-michelson_v1_primitives-for-coq into proto-proposal

Reopening of !240 (merged)

Small changes to two files which so that they compile in Coq:

  • break mutual dependency between types which actually are not mutually dependent;
  • add @coq_axiom to ignore some failing functions (the current fix would incur a performance cost).

Part of a larger goal to compile the protocol in Coq as it is (nomadic-labs/tezos#161).

Merge request reports