Rename labels to be more consistent.

1 files changed, 4 insertions, 4 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
index c94f388..af652a1 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -32,11 +32,11 @@
       \infer1{\jdgmnt{ty}{\Psi}{\mu X. A}}
     \end{prooftree}
   \]
-  \caption{Well-formedness of \lang{} types}\label{fig:artist-wf}
+  \caption{Well-formedness of \lang{} types}\label{fig:lang-wf}
 \end{figure}
 
 In this section we introduce \lang{}, a simply-typed lambda calculus
-with \emph{regular types}.  \Cref{fig:artist-wf} shows the
+with \emph{regular types}.  \Cref{fig:lang-wf} shows the
 well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means
 that \(A\) is a type using variables from \(\Psi\). We have labelled
 \(n\)-ary products and sums, where the set of labels is finite. Types
@@ -124,10 +124,10 @@ claim the type unrepresentable in some models of System~T}.
     }
   \end{array}
   \]
-  \caption{Typing judgements for \lang{}}\label{fig:artist-types}
+  \caption{Typing judgements for \lang{}}\label{fig:lang-ty}
 \end{figure}
 
-\Cref{fig:artist-types} gives the typing judgements for \lang{}. The
+\Cref{fig:lang-ty} gives the typing judgements for \lang{}. The
 introduction and elimination rules for functions, products and sums
 are standard, as are the rules for variables and let bindings. The two
 new operators, \roll{} and \foldkw{}, introduce values of an inductive