Skip to content

We have ambiguous coercion paths

When compiling with Coq master, we see lots of these:

[constRF; rFunctor_diag] : cmraT >-> Funclass
[ucmra_cmraR; constRF; rFunctor_diag] : ucmraT >-> Funclass

Also see e.g. this build log.

Is this a problem? Can we do anything about it?