diff --git a/spec/doc.tex b/spec/doc.tex
index b1673e3f5402d58d4a0867a4c065f07011d4c7f9..aadf79b08c69fd2efef247b1f197eb2a60403246 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -722,8 +722,7 @@ have an arbitrary order after instantiation.
 Nevertheless, consumers of Alethe must consider the possible
 implicit reordering of equalities.
 
-% PF TODO why concrete?  Why not simply call it Semantics?
-\section{The Concrete Semantics}
+\section{The Semantics of Alethe}
 \label{sec:semantic}
 
 Most of the content is taken from the presentation and the correctness proof of