Typing error when parsing FA2 LIGO contract
The LIGO implementation of the FA2 multi-asset contract (attached) appears to generate a typing error in Mi-Cho-Coq:7
COQC fa2_string.v COQC fa2_parse.v = "Lexing: OK Parsing: OK Expansion: OK Type checking: Typing error
The typing error does not occur when running tezos-client typecheck script, only in Mi-Cho-Coq. There the code generates a typing error on lines 730 and 1089.