Quentin VERMANDE
Quentin VERMANDE
I did `nix-shell --no-out-link --argstr bundle "coq-8.20" --argstr job "coqeal"` in my local repo with `master` checked out and got the exact same issue in `coqeal`. Does that mean the...
I see, there is an elpi version issue. On master, it simplifies a term before counting the number of products it has, whereas on `2.2.0`, it returns `0` no questions...
Ah, hence the rebase. So hopefully it works and we run only one CI.
As long as we copy everything in `ssralg`, we should keep the documentation, should we not?
The comments should be addressed. I added iterated products in `monoid.v`, in the end.
Is it right that there should eventually be no `Reserved Notation` outside of `ssrnotations.v` and that every file should import it instead of reserving notations?
I do not know which ones you want to reserve, I did "^*", tell me if you want me to do other ones.
I see, adding `left associativity` in `fingroup.v` somewhere solved it. I check that everything still compiles and if so I push.
My first round of overlays should be ready soon. Is there something to do here (e.g. rerunning the CI if it is fixed)?
https://github.com/MetaRocq/metarocq/pull/1152 is only a small performance improvement, so I think we might as well retry the CI now.