The Coq team announced a rename months ago, but there is no sign of it on the webpage. This is silly!
The present PR adds just a couple mentions of the new Rocq name, enough for people to know that this is happening for real -- but not enough that it is a lot of work or that tricky questions have to be answered for consistency.
The proposed explanation includes an invitation to use the combined name "Coq/Rocq" during a transition period, so that people that only know of the old name (that is, almost everyone) does not get lost. This is used on the webpage itself, whose title is now "The Coq/Rocq proof assistant."
gasche
commented
3 months ago
The Coq team announced a rename months ago, but there is no sign of it on the webpage. This is silly!
The present PR adds just a couple mentions of the new Rocq name, enough for people to know that this is happening for real -- but not enough that it is a lot of work or that tricky questions have to be answered for consistency.
The proposed explanation includes an invitation to use the combined name "Coq/Rocq" during a transition period, so that people that only know of the old name (that is, almost everyone) does not get lost. This is used on the webpage itself, whose title is now "The Coq/Rocq proof assistant."