Broken with math-comp master

imdea-software / fcsl-pcm

Partial Commutative Monoids

Apache License 2.0

25 stars 12 forks source link

Closed ejgallego closed 5 years ago

ejgallego commented 5 years ago

Hi folks,

as per @ggonthier detailed analysis here, current fcsl-pcm is broken in math-comp master which in turn makes it broken in Coq's CI.

Could you please apply the suggested fix?

Thanks!

anton-trunov commented 5 years ago

Hi @ejgallego! Thanks for opening the issue. I incorporated the fix by @ggonthier (thank you) in f65fa08de125cf5b76de66f439ef977b4edb6061.

ejgallego commented 5 years ago

Thanks @anton-trunov for the quick response!