affeldt-aist

Thank you for the quick answer. At least, this is a clear assessment of the situation.

> I did not read the PR but one should ideally show that the type `angle` whatever its definition is a ring quotient of `R` by the ideal `2pi` Right...

This PR is the consequence of an effort to replace the coq-robot definition of trigonometric functions with what is now available in MathComp-Analysis but maybe we should first generalize expR...

Could you put some information in the changelog? (At least about the potentially breaking changes.) In any case, good to see things get little bit tidier. Thanks!

Congratulations! I'm looking forward to reading your paper. We are interesting in integrating it and I am willing to spend time on it. Maybe the easiest way is to PR...

Thank you for your interest We were planning to look into the automated nix support provided by the coq-community https://github.com/coq-community/coq-nix-toolbox

Thank you for your interest! monae uses infotheo for probabilities and infotheo uses fields for error-correcting codes (in a limited way) iirc, hence the dependency on `mathcomp-field`, which triggers the...

You can also observe that the subdirectory `impredicate_set` contains a subset of monae (code is duplicated almost verbatim) without the probabilities-related stuff (because in the current state of affairs it...

> What can I start from? I did a tentative split as PR #57 . It turns out that some files that are not explicitly depending on probabilities still depend...

> I've removed some unused dependencies on infotheo in #59 Thank you for the careful review! > As for the real dependencies that are still there, I've noticed the following:...