Anton Trunov

Hi @CohenCyril, yes, a better error message would be great! Is this limitation documented somewhere? If not, it would be great to have that too.

FWIW, here is a somewhat related issue: https://github.com/coq/opam-coq-archive/issues/954.

@Lysxia What would be the best way to implement this? As a `QCExtractionPath` vernacular or some other way?

We started using `Cmdliner` for the Scilla formatter `scilla-fmt`: it looks great, although, it uses double dashe `--` for long CLI arguments and the Scilla checker and runner use single...

Since identifiers contain extra information, like locations, we should decide if the `Comparable` implementation should just ignore that part.

There is some attempts to implement something like this here: https://github.com/Zilliqa/scilla/blob/55f1b64dba4db9096acea243e0e71aaa3029d3aa/src/base/Type.ml#L89

Related issue: #438

Related: we now have an annotation mapper in https://github.com/Zilliqa/scilla/blob/master/src/base/SyntaxAnnotMapper.ml.

Ok, this has been done. Relevant discussion starts here -- https://github.com/coq-community/manifesto/issues/55#issuecomment-564969619.

You are right. I guess I missed that addition. Thanks.