Enzo Crance
Enzo Crance
The error seems to come from the lift (https://github.com/LPCIC/coq-elpi/pull/388). I haven't added tests, but maybe we should (would just require forging a few `indt-decl` values by hand).
Issue https://github.com/LPCIC/coq-elpi/issues/374 might be related as the error message is the same.
I took some time to investigate. I think I found the bug. *Short: a lift is needed, but only for indices mentioning uniform parameters.* Consider the following inductive type: ```coq...
Both `test_invert.v` and my code seem to work with the selective lift update.
I think this bug came from the fact I tried to edit `poly` in [this line](https://github.com/LPCIC/coq-elpi/blob/aa3f4b47841e752292e4961cc742511035822ae4/src/coq_elpi_builtins.ml#L1873), so *maybe* I opened an issue that does not concern `master`, and if that's...
> sorts have a super, not universes There is `Univ.Universe.super` and `Sorts.super`, I do not really know the difference.
I would have liked to add the following test to `test_API_typecheck.v`: ```coq Elpi Query lp:{{ coq.typecheck (sort (typ U)) T ok, coq.unify-eq T (sort (typ {coq.univ.super U})) ok. }}. ```...
> reimplementing `zify` in Coq-elpi Learning Coq-elpi and working on this are my main goals in the short term future. I would be glad to talk about this with you...