Ali Caglayan

@coq/typeclasses-maintainers What is the correct way to restrict this instance short of removing it?

FTR `Numeral Notation` has been replaced with `Number Notation`. Also, we have been using -noinit successfully in the HoTT library for some time now. If you need any help enabling...

@coqbot merge now

What milestone do I set?!

Please fix CI.

Why do we have to generate the rules ourselves? This seems like a waste of time. Wouldn't it be better to just push for the feature of dune that allows...

@ejgallego Please resurrect this.

I am currently rebasing, but it is not so easy, there are a lot of big changes that happened in the mean time. I am optimistic though.

@ejgallego OK thanks. How do I fix the META stuff? I ended up changing back to "ltac_plugin" in my own attempts.

It's not the end of the world to force push to a closed PR, there are workarounds: https://gist.github.com/robertpainsi/2c42c15f1ce6dab03a0675348edd4e2c GItHub just checks the commit hash from when the PR was closed.