X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=db743fc9a049d716c931747ca7cb09180723980a;hp=fbad0ea11f481bdf1b0c061ea92c0f0b2fea7895;hb=b1a9ce14b51423bf676df768278fd6b6d6579ca1;hpb=bff5a598be513f497ad61d29b7c7584f94d2b993

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index fbad0ea..db743fc 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -1610,8 +1610,7 @@
         simply inline the let bindings that have a polymorphic type,
         which should (eventually) make sure that the polymorphic
         expression is applied to a type and/or dictionary, which can
-        \refdef{beta-reduction}
-        then be removed by β-reduction.
+        then be removed by β-reduction (\in{section}[sec:normalization:beta]).
 
         Since both type and dictionary arguments are not representable,
         \refdef{representable}
@@ -1713,7 +1712,7 @@
         η-abstraction also introduces extra applications (the application of
         the let expression to \lam{q} in the above example). These
         applications can then propagated down by the application propagation
-        transformation (\in{section}[sec:normalization:approp]). In our
+        transformation (\in{section}[sec:normalization:appprop]). In our
         example, the \lam{q} and \lam{r} variable will be propagated into the
         let expression and then into the case expression: