Frédéric Besson

Hello, ppsimpl has indeed some support for mathcomp. The list of operators that are currently supported can be seen in the source by looking at the file Buildmathcomp.v. From what...

It should be in the branches 8.7 or 8.8 git clone https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git ppsimpl cd ppsimpl git checkout -b ppsimpl-8.8 origin/ppsimpl-8.8

I really hope so. Though, I considered that it was a bit too soon to advertise the extensibility... If you wish to have a look the relevant files are -...

> * `zify` doesn't work for overloaded operators, e.g., `@eq_op bool_eqType : bool -> bool -> bool` and `@eq_op nat_eqType : nat -> nat -> bool`. (When I tried to...

@pi8027 , ping me when you report the issue for overloading.

Thanks for the report. This is a regression. This used to work e.g 8.13.2.

Hi, From the start, I did not consider parametric instances to be in the scope of `zify`. I would expect the generalisation to break a lot of `zify`. I acknowledge...

> Oh, so it wouldn't work if the binary operator has implicit parameters. Actually, there is some support for implicit parameters. This is needed to support `ssreflect`: matching works with...

> > @fajb is this the expected behavior for saturate? I was thinking the hypotheses would only be added if the premises were provable without case analysis or similar. >...

Using only known premises by default looks reasonable. I suspect there will be a few regressions due to `Saturate Z.pow` but this is probably an acceptable price. Next question is...