Index: Deliverables/D3.4/Report/report.tex
===================================================================
--- Deliverables/D3.4/Report/report.tex (revision 3236)
+++ Deliverables/D3.4/Report/report.tex (revision 3249)
@@ -102,11 +102,16 @@
-\cerco{} Work Package 3, \emph{Verified Compiler - front end} aims
-for formalise and verify the front-end of the \cerco{} cost lifting
-compiler. This document accompanies the final deliverable,
-\textbf{D3.4: Front-end Correctness Proofs}. The deliverable consists
-of the formal correctness proofs for the front-end, written in the
-\matita{} proof assistant and this document provides report on the
-work carried out for it.
+This document reports on \textbf{D3.4:~Front-end Correctness Proofs}, the
+final deliverable of \cerco{} work package~3 \emph{Verified Compiler - front
+ end}. That work package was devoted to the formalisation and verification of
+the front-end of the \cerco{} cost lifting compiler, and Deliverable~3.4 is a
+machine-checked formal correctness proof of the compiler front-end, written in
+the \matita{} proof assistant.
+
+The proof itself is contained in a series of Matita files, listed in
+Appendix~A and culminating in the lemma \lstinline'front_end_correct' and the
+theorem \lstinline'correct' in the file \lstinline'correctness.ma'. This
+document accompanies the deliverable and briefly reports on the work carried
+out in the development of that proof.
\vspace*{1cm}
@@ -802,5 +807,5 @@
we consider is an $8$-bit one. In \textsf{Clight}, casts are
expressions. Hence, most of the work of this transformation
-proceeds on expressions. The tranformation proceeds by recursively
+proceeds on expressions. The transformation proceeds by recursively
trying to coerce an expression to a particular integer type, which
is in practice smaller than the original one. This functionality