Skip to content

Renaming to avoid name collisions in Coq

Guillaume Claret requested to merge guillaume-claret@renaming-to-avoid-collisions into proto-proposal

We do various renaming in order to prevent name collisions in the Coq translation of the protocol using coq-of-ocaml. Indeed, Coq does not support multiple definitions of the same variable name at top-level.

Part of the larger task https://gitlab.com/nomadic-labs/tezos/-/issues/199 to compile the Michelson interpreter in Coq.

Merge request reports