diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 1f2aa1d8c70b1c7c8ac694c145a2268c8c79f9c1..9d90521d793eb9a719a2f745524065fea11619a8 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -702,6 +702,9 @@ architectures and error correcting schemes to the system
 
 \REM{stuff about WP 2 here}
 
+\oldt{\benREM{This
+  paragraph needs refactoring, but I need Belen's input to make a
+  vaguely coherent new text}
 Since the overall goal of the project is to produce a
 \emph{retargetable} compiler, able to generate executables for
 multiple architectures, these differing characteristics must be taken
@@ -714,28 +717,27 @@ characteristics and architectural constraints of various idealised and
 realistic machines, and develop language features of \azx to express
 these properties.  The goal is two-fold: to facilitate
 \emph{code-generation} for a given machine from an \azx term; and to
-expose information needed by the \emph{optimiser}.
+expose information needed by the \emph{optimiser}.}
 
-
-\oldt{
-  A key research challenge of this work package consists in the
+A key research challenge of this work package consists in the
 management of the {\em classical computation} and {\em classical
   information} within quantum algorithms: What computation should
 occur at the \azx-generation phase, and which classical parameters are
-passed on to the \azx terms? To help answer this question we will
-design a test suite (\ref{task:testBench}) to compare possible
-solutions.
-
-
+passed on to the \azx terms? Task \ref{task:betterboxes} focuses on
+the question of tests based on measurement results: how should they be
+integrated within \azx?
+%
 While in the early stages of the project, it will already be quite
 useful to study concrete diagrams of fixed size (e.g. a quantum
 circuit on $N$ qubits for a previously-fixed $N$), in task
-\ref{task:betterboxes}, we will extend \azx to support parametrised
+\ref{task:axioms}, we will extend \azx to support parametrised
 families of diagrams (e.g. quantum circuits with $N$ qubits where $N$
 can vary) mirroring the control structures present in a quantum
 HLL. This will enable more sophisticated, generic optimisations to be
 run in advance of needing any particular computational procedure.
-}
+The test suite designed in~\ref{task:testBench}
+will be used to compare and choose amongst the possible solutions.
+
 
 
 \subsubsection{Machine-independent optimisation}