Simplify title

1 files changed, 2 insertions, 2 deletions

diff --git a/proof.tex b/proof.tex
index e54a9af..a02baf9 100644
--- a/proof.tex
+++ b/proof.tex
@@ -1,6 +1,6 @@
-\section{Semantics Preservation Proof of Translation}\label{sec:proof}
+\section{Correctness Proof}\label{sec:proof}
 
-\JW{That's quite a hard-to-parse section heading; I'd go for something simpler like `Correctness Proof' or `Proving Correctness'}
+%\JW{That's quite a hard-to-parse section heading; I'd go for something simpler like `Correctness Proof' or `Proving Correctness'}
 
 Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to formally prove the correctness of our C-to-Verilog compilation.  This section describes the main correctness theorem that was proven and the key ideas in the proof. The full Coq proof is available online~\cite{yann_herklotz_2021_5093839}.