Compatibility with Coq 8.8? about category-theory HOT 8 CLOSED

8.8 is now supported.

from category-theory.

It is not compatible yet. I have an item on my own private task list to report some bugs against the Coq tracker for things like the above. It's not that hard to move past the issue you're seeing now by defining the body of the list equivalence separately, but then you'll just run into another anamoly a bit further down the file.

from category-theory.

I'm still using Coq 8.7 for all my uses of this library, but I think that moving to 8.8 should become a priority now.

from category-theory.

Okay, thanks for getting back to me so quickly!

from category-theory.

@siddharthist I'm more interrupt driven than I like to think, but your questions have prompted me to create those bugs today. Running the bug minifier now, and will update this issue to point to the Coq bug once created.

from category-theory.

Logged as coq/coq#8004

from category-theory.

Once you get this working with 8.8 / master, you should add it to Coq's CI so that it doesn't accidentally break.

from category-theory.

@JasonGross How does one add something to Coq's CI?

from category-theory.