> It needs a quirks $stem_extensions entry to cover the renaming, and > compcert BDEP needs changing. ........ >> The coq project has been renamed to rocq. I'd like to reimport it as >> math/rocq before doing more updates.
thanks Daniel and stu! I understand now that access to github.com/coq/coq is redirected to github.com/rocq-prover/rocq. As far as I remember, when rocq repository was created, it was an independent repository different from coq. That made me thinking about adding math/rocq with the newer version and keeping math/coq for a while until lang/compcert being updated to depend on math/rocq. -- yozo.
