Skip to content

Avoid non-top-level uses of 'let and' constructs for coq-of-ocaml

Guillaume Claret requested to merge guillaume-claret@avoid-non-toplevel-let-and into proto-proposal

Reopening of !238 (merged)

Avoid non-top-level uses of let and constructs for coq-of-ocaml (not supported in Coq), by either:

  • rewriting it if it trivial;
  • adding a @coq_axiom attribute to ignore it.

We prefer not to rewrite large functions for now as this may require a measure of the performance impact. Part of a larger task https://gitlab.com/nomadic-labs/tezos/-/issues/161 to lint the protocol for coq-of-ocaml.

Merge request reports