bmsherman/topology

Coercions should be explicitly imported

Closed this issue · 4 comments

bmsherman commented

I don't have time to do this. Is it a workable solution to just drop this project from the CI test suite?

maximedenes commented

Is it a workable solution to just drop this project from the CI test suite?

Indeed I think this is the only solution for now, as this has blocked some desirable clean-ups on the Coq side for some time already.

On the longer term, I think @Zimmi48 suggested this development could be moved to coq-community. I'll let him say more about it.

  • 👍1
Zimmi48 commented

Indeed, since, as far as I understand, this project is not actively developed anymore, it could be transferred to coq-community if it can find a new maintainer there. Have a look at the manifesto. If you think it makes sense, you could open a new issue to advertise that this project is looking for a new maintainer.

ppedrot commented

Let's close this since it's not in the CI anymore.