Index: /src/ASM/CPP2011/cpp-2011.tex
===================================================================
--- /src/ASM/CPP2011/cpp-2011.tex (revision 1023)
+++ /src/ASM/CPP2011/cpp-2011.tex (revision 1024)
@@ -223,5 +223,5 @@
For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$.
This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
-In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated than that of Coq.
+In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
% ---------------------------------------------------------------------------- %
@@ -283,13 +283,8 @@
This is a tempting approach to the proof, but ultimately the wrong approach.
-In particular, to expand a pseudo instruction we need to know the address
-at which the expanded instructions will be located, for instance to determine
-if a short jump is possible. That address is a function of the
-\emph{object code} generated for the pseudo-instructions already visited.
-Thus we need to assemble each pseduto instruction down to object code before
-moving to the next one and this must be eventually reflected on the proof
-of correctness. Therefore we will have lemmas for the \texttt{assembly1}
-function and for the composition of \texttt{expand\_pseudo\_instruction} and
-\texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone.
+In particular, to expand a pseudoinstruction we need to know the address at which the expanded instructions will be located, for instance to determine if a short jump is possible.
+That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded.
+Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness.
+Therefore we will have lemmas proving correctness for the \texttt{assembly1} function, and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone.
% ---------------------------------------------------------------------------- %