error when building ecc_modern

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

error when building ecc_modern #59

Closed lambdaofgod closed 2 years ago

lambdaofgod commented 3 years ago

I tried to build infotheo using make:


COQC ecc_modern/ldpc_algo.v
File "./ecc_modern/ldpc_algo.v", line 175, characters 0-76:
Error: ConstructiveCauchyReals.CReal is not an inductive type.

garrigue commented 3 years ago

Which Coq version are you using?

affeldt-aist commented 3 years ago

Maybe you are running Coq < 8.13. (I think we got this error when upgrading from 8.12 to 8.13.)