> 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.