Skip to content

Avoid a name collision for `encoding` in the generated Coq

Avoid a name collision in tez_repr.ml for the value encoding in the generated Coq. Indeed, this value is both present in the include and defined at top-level. This generates an error in Coq as it does not allow re-definitions at top-level.

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

Edited by Mehdi Bouaziz

Merge request reports