Thibaut Pérami

I may do it myself, but I've never written a Coq plugin, so I have no idea how to call something like `setoid_rewrite` from OCaml or how to access the...

Right now I'm quite busy, but I may consider it in a few month

Oh, so it wouldn't work if the binary operator has implicit parameters. Maybe we can just do the same ad-hoc version but that associate the typeclass instance with parameters to...

Ok so I moved on a completely different project that doesn't need this, I might consider it if I come back to a project that needs this (which is possible,...

In my use case, the bitvector size are not the same everywhere, but they are known and fixed (they do not depend on some unknown variable) so I would need...

Interesting, I stopped at having `Add Zify InjTyp I1` run successfully, I didn't try to actually use it with `lia`.

Hi, Sorry if this was already planned, but since it seems to me that this was fixed more than 2 months ago, do you think it would be possible to...