search

affeldt-aist / monae

Monadic effects and equational reasonig in Coq
GNU Lesser General Public License v2.1
68 stars 12 forks source link

trying to use infotheo_hb #99

Closed affeldt-aist closed 1 year ago

affeldt-aist commented 2 years ago

@t6s

affeldt-aist commented 2 years ago

@t6s there shouldn't be any FIXME left, maybe time to check the documentation?

affeldt-aist commented 2 years ago

@t6s To make the impredicativity subdirectory compile with coq 8.16, the top line of the offending file should change to

Declare ML Module "coq-paramcoq.plugin".