imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

Broken by mathcomp change #17

Closed SkySkimmer closed 4 years ago

SkySkimmer commented 4 years ago

https://github.com/math-comp/math-comp/commit/d60c67b8f33f55e11ca159246d2a447102f10f20 "Change the order of arguments in ltngtP" used https://github.com/imdea-software/fcsl-pcm/blob/e565b808d26ee63f296f672721c6e68de27ec677/pcm/natmap.v#L296 (and perhaps elsewhere)

Note that this breaks Coq's CI

anton-trunov commented 4 years ago

Should be fixed now

anton-trunov commented 4 years ago

Ok, looks like the fix works. Closing this issue for now. Feel free to reopen.