Missing API on universes #544
Conversation
|
Given that Trocq that needs this PR has joined Coq-community, could you comment on the feasibility of merging it in the near future @gares? If it's not feasible, we may be faced with maintaining a fork of Coq-Elpi in Coq-community, which would be unfortunate for everyone involved. Other solution suggestions also welcome. |
|
I'm all for helping out but this PR breaks ci, I did not even look into it to be honest, since I did not know there was any urgency |
|
There is no huge urgency really, it's more about deciding whether we would need to fork Coq-Elpi in Coq-community just to be able to test and package Trocq. Maybe you can say something about when you might have time to take a look at the PR assuming it's not urgent, and then we can decide after that. |
|
Is my understanding correct, that this is waiting for progress on algebraic universes? |
@gares @ecranceMERCE would it make sense to merge this upstream?