compatibility with mca 0.4.0 and greater

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes

GNU Lesser General Public License v2.1

64 stars 15 forks source link

Closed affeldt-aist closed 2 years ago

affeldt-aist commented 2 years ago

I have reintroduced choice_of_Type but that should be better to rely only on MathComp-Analysis for that. @t6s