Require Znumtheory before using it#60
Conversation
|
|
Dear maintainers, Do you consider this PR acceptable enough to merge it so that the related stdlib change can progress? Thanks! |
|
We should fix CI before merging this, but I don't have time to do it right now. Ping @math-comp/core |
|
Ack. Looks like the ping did not highlight, so maybe it didn't work. (Also note that the change itself is trivial -- unless |
|
CI fixed but for one CI target where the docker image is still work in progress (AFAIU). LGTM. Let's merge! |
The ping did work but I guess most of the team was on vacation or something... |
|
Thanks! |
For rocq-prover/stdlib#136