diff --git a/incl/footer.html b/incl/footer.html index 3ede9ae2a7..0b3b9e79d1 100644 --- a/incl/footer.html +++ b/incl/footer.html @@ -14,7 +14,8 @@

Recent news

October 2023: we have decided to rename 'Coq' into 'The Rocq Prover'. Renaming all existing resources is a lot of work, it will be a slow, gradual transition. - During this transition period, please feel free to mention the proof assistant as Coq/Rocq. + During this transition period, please feel free to use both names, for example + by writing "formalized with Rocq (formerly Coq)" or "formalized with Coq (also named Rocq)".

diff --git a/incl/header.html b/incl/header.html index 5d641f118f..d60342a823 100644 --- a/incl/header.html +++ b/incl/header.html @@ -3,7 +3,7 @@ - <#TITLE> | The Coq/Rocq Proof Assistant + <#TITLE> | The Coq Proof Assistant, the Rocq prover @@ -30,7 +30,7 @@ -

The Coq/Rocq Proof Assistant

+

The Coq (Rocq) Proof Assistant