Quentin VERMANDE
Quentin VERMANDE
Sorry for the delay, I ever so stupidly deleted the code, so I did it again, and I currently have very few time I can spend on this. I opened...
Thank you for looking into it. With the current algorithm, unification of `proj _` with something always (afaikt) uses canonical structures, which in my usecase introduces unification variables, which causes...
> There are failures in the test suite, do you want to see the full CI anyway? No, I forgot that I had access to the test suite locally, I...
> I guess the change is that in > > ```coq > Set Primitive Projections. > Record R := { foo : nat; bar : nat }. > > Canonical...
Sorry for the delay, and thank you for your comments. Please @pi8027 ignore this PR for now. I needed preorders for a personal project and I figured I might as...
The splitting is done, the only thing left to do is make it backwards compatible. Most notably, "a few" names were moved to `preorder.Preorder`. I would like to have them...
I was afraid you would say that, I guess there is no way around it then. I am on Coq and HB master (4b52a0d917 and 5f37676 respectively). It is slow...
Right, if I manage to get to the point where the CI is happy, I will do that.
I added a test in `test_order_conv.v` for `preorderType`, which works, so I am very confused by the failure for `porderType`. I tried messing around with unification tests to get a...
> > Meanwhile, maybe you can work around it by replacing HB.saturate with some manual HB.instance as done by @pi8027 in its previous semilattive PR, but not sure it's worth...