From e3974f32ec8b38102a632ec7b1e002b6713f63b7 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Fri, 5 Jul 2024 09:48:34 +0200 Subject: [PATCH] new iteration after feedback from silene --- incl/footer.html | 3 ++- incl/header.html | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) 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