Index: doc/theses/mike_brooks_MMath/array.tex
===================================================================
--- doc/theses/mike_brooks_MMath/array.tex	(revision 5e8d75bbda1b63dfcc63fb0a003758c17cc3fae5)
+++ doc/theses/mike_brooks_MMath/array.tex	(revision 38e17b075cc18efa0ede32a63ca235bf8f4b3072)
@@ -90,5 +90,5 @@
 
 
-\section{Dependent typing}
+\section{Dependent Typing}
 
 General dependent typing allows the type system to encode arbitrary predicates (\eg behavioural specifications for functions),
@@ -103,5 +103,5 @@
 
 
-\section{Features added}
+\section{Features Added}
 
 This section shows more about using the \CFA array and dimension parameters, demonstrating their syntax and semantics by way of motivating examples.
@@ -782,5 +782,5 @@
 
 
-Figure~\ref{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
+\VRef[Figure]{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
 It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafe.
 It also shows that C-incompatibilities only occur in cases that C treats unsafe.
@@ -859,5 +859,5 @@
 
 
-\section{Multidimensional array implementation}
+\section{Multidimensional Array Implementation}
 \label{s:ArrayMdImpl}
 
@@ -978,5 +978,5 @@
 \end{figure}
 
-Figure~\ref{fig:subscr-all} shows one element (in the shaded band) accessed two different ways: as @x[2][3]@ and as @x[all][3][2]@.
+\VRef[Figure]{fig:subscr-all} shows one element (in the shaded band) accessed two different ways: as @x[2][3]@ and as @x[all][3][2]@.
 In both cases, value 2 selects from the coarser dimension (rows of @x@),
 while the value 3 selects from the finer dimension (columns of @x@).
@@ -1024,5 +1024,5 @@
 % The choice to implement this style-1 system upon C's style-2 arrays, rather than its style-3 pointer arithmetic, reduces the attack surface of unsafe code.
 % My casting is unsafe, but I do not do any pointer arithmetic.
-% When a programmer works in the common-case style-2 subset (in the no-@[all]@ top of Figure~\ref{fig:subscr-all}), my casts are identities, and the C compiler is doing its usual displacement calculations.
+% When a programmer works in the common-case style-2 subset (in the no-@[all]@ top of \VRef[Figure]{fig:subscr-all}), my casts are identities, and the C compiler is doing its usual displacement calculations.
 % If I had implemented my system upon style-3 pointer arithmetic, then this common case would be circumventing C's battle-hardened displacement calculations in favour of my own.
 
@@ -1067,5 +1067,5 @@
 
 
-\section{Bound checks, added and removed}
+\section{Bound Checks, Added and Removed}
 
 \CFA array subscripting is protected with runtime bound checks.
@@ -1089,5 +1089,5 @@
 
 
-\section{Array lifecycle}
+\section{Array Lifecycle}
 
 An array is an aggregate, like a structure;
@@ -1341,5 +1341,5 @@
 % note to Mike, I have more fragments on some details available in push24\fragments\uNoCtor.txt
 
-\section{Comparison with other arrays}
+\section{Comparison with Other Arrays}
 
 
@@ -1457,5 +1457,5 @@
 
 
-\subsection{Levels of dependently typed arrays}
+\subsection{Levels of Dependently Typed Arrays}
 
 The \CFA array and the field of ``array language'' comparators all leverage dependent types to improve on the expressiveness over C and Java, accommodating examples such as:
@@ -1504,16 +1504,16 @@
 Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark.
 
-\subsection{Static safety in C extensions}
-
-
-\section{Future work}
-
-\subsection{Declaration syntax}
-
-\subsection{Range slicing}
-
-\subsection{With a module system}
-
-\subsection{With described enumerations}
+\subsection{Static Safety in C Extensions}
+
+
+\section{Future Work}
+
+\subsection{Declaration Syntax}
+
+\subsection{Range Slicing}
+
+\subsection{With a Module System}
+
+\subsection{With Described Enumerations}
 
 A project in \CFA's current portfolio will improve enumerations.
@@ -1602,5 +1602,5 @@
 In the case of adapting this pattern to \CFA, my current work provides an adapter from ``successively subscripted'' to ``subscripted by tuple,'' so it is likely that generalizing my adapter beyond ``subscripted by @ptrdiff_t@'' is sufficient to make a user-provided adapter unnecessary.
 
-\subsection{Retire pointer arithmetic}
+\subsection{Retire Pointer Arithmetic}
 
 
@@ -1614,5 +1614,5 @@
 (For later:  That's what I offer with array.hfa, but in the future-work vision for arrays, the fix includes helping programmers stop accidentally using a broken C-ism.)
 
-\subsection{\CFA features interacting with arrays}
+\subsection{\CFA Features Interacting with Arrays}
 
 Prior work on \CFA included making C arrays, as used in C code from the wild,
