Skip to content

[michocoq] Avoid redefining `False` in `util.v`

Raphaël Cauderlier requested to merge rafoo@False_shadowing into dev

The name of the Michelson data constructor False clashes with the Coq proposition for contradiction. To avoid qualifying the Coq proposition, util.v redefines it so util.False is defined as Logic.False. This has unpleasant side effects (see #53 (closed)) so we remove this definition and qualify the name in the few places where it is used instead.

Closes #53 (closed).

Merge request reports