diff --git a/grammar/grammar.tex b/grammar/grammar.tex
index c3ee82c..e922c83 100644
--- a/grammar/grammar.tex
+++ b/grammar/grammar.tex
@@ -15,9 +15,9 @@ modifications:
     \begin{itemize}
       \item Litteral records are always atomic (\emph{ie} only have one field). An
         \emph{orthogonal merge} operator ($\orthplus$) allows building complex
-        records~\footnote{We still often write \{ $x_1$ = $y_1$; $\cdots{}$;
-        $x_n$ = $y_n$ \} as a shorthand for \{ $x_1$ = $y_1$; \} $\orthplus
-        \cdots{} \orthplus$ \{ $x_n$ = $y_n$; \}},
+        records~\footnote{We still often write \{ $s_1$ = $y_1$; $\cdots{}$;
+        $s_n$ = $y_n$ \} as a shorthand for \{ $s_1$ = $y_1$; \} $\orthplus
+        \cdots{} \orthplus$ \{ $s_n$ = $y_n$; \}},
 
       \item The syntax in nix for a recursive definition of records (\texttt{\{ x.y
         = 1; x.z = 2; \}}) doesn't exist anymore,
diff --git a/semantics/semantics.tex b/semantics/semantics.tex
index ae0cb59..e1360db 100644
--- a/semantics/semantics.tex
+++ b/semantics/semantics.tex
@@ -57,7 +57,7 @@ figure~\pref{fig:semantics:nix-light:patterns}
     \bfseries
     <E> ::= [] \| \meta{E e}
     \alt \meta{E.a} \| \meta{E.a} or \meta{e} \| \meta{v.F} \| \meta{v.F} or \meta{e}
-    \alt \{ \x/ = \e/; \ldots{}; \x/ = \e/; \E/ = \e/; \ldots{}; \e/ = \e/ \}
+    \alt \{ \v/ = \e/; \ldots{}; \v/ = \e/; \E/ = \e/; \ldots{}; \e/ = \e/ \}
     \alt with \E/; \e/ | if \E/ then \e/ else \e/
 
     <F> ::= \E/.\a/ \| \v/.\meta{F}
diff --git a/typing/recordTypingRules.tex b/typing/recordTypingRules.tex
index 4424f36..4a461ca 100644
--- a/typing/recordTypingRules.tex
+++ b/typing/recordTypingRules.tex
@@ -1,18 +1,18 @@
 \inferrule{%
-  \Γ \vdash e : \τ \\
-  \Γ \vdash l : \bigvee\limits_{i=1}^n s_i
+  \Γ \vdash e' : \τ \\
+  \Γ \vdash e : \bigvee\limits_{i=1}^n s_i
 }{%
-  \Γ \vdash \left\{ l = e; \right\} :
+  \Γ \vdash \left\{ e = e'; \right\} :
   \bigvee\limits_{i=1}^n \left\{ s_i: \τ \right\}
 }
 \irlabel{RFinite}
 \and
 \inferrule{%
-  \Γ \vdash e : \τ \\
-  \Γ \vdash l : \σ \\
+  \Γ \vdash e' : \τ \\
+  \Γ \vdash e : \σ \\
   \σ \subtype \ty{string}
 }{%
-  \Γ \vdash \left\{ l = e; \right\} :
+  \Γ \vdash \left\{ e = e'; \right\} :
   \left\{ \_: \τ \vee \undef \right\}
 }
 \irlabel{RInfinite}
diff --git a/typing/records.tex b/typing/records.tex
index 218e611..0857b66 100644
--- a/typing/records.tex
+++ b/typing/records.tex
@@ -14,7 +14,7 @@ We assume a record language, whose grammar is defined as follows:
     \| \e/ $\orthplus{}$ \e/
     \| \e/ \textbackslash{} \e/
     \| \e/.\e/
-    \| l
+    \| s
 \end{grammar}
 
 Where:
@@ -24,11 +24,11 @@ Where:
   \item $\orthplus{}$ denotes the merge of two records, assuming no field is
     defined in both,
   \item \textbackslash{} denotes the removal of a field (\emph{ie} $e_1
-    \backslash e_2$ is the record $e_1$ whose field $l$ is undefined, where $l$
+    \backslash e_2$ is the record $e_1$ whose field $s$ is undefined, where $s$
     is the value of $e_2$).
-  \item $e_1 . e_2$ denots the access to the field $l$ of the record $e_2$,
-    where $l$ is the value of $e_2$.
-  \item $l$ range over the set of allowed value labels (which here will be \ty{string})
+  \item $e_1 . e_2$ denots the access to the field $s$ of the record $e_2$,
+    where $s$ is the value of $e_2$.
+  \item $s$ range over the set of allowed value labels (which here will be \ty{string})
 \end{itemize}
 
 \section{Static labels}
@@ -78,7 +78,7 @@ all as evaluation of labels was a no-op
 
 The most logical choice seems to evaluate every label eagerly as soon as we
 need the value of one of them. This entails that record values will have the
-form \texttt{\bfseries \{ $l$ = $e$; \ldots{}; $l$ = $e$; \}} where $l$ designs
+form \texttt{\bfseries \{ $s$ = $e$; \ldots{}; $s$ = $e$; \}} where $s$ designs
 an evaluated label (a string value). The semantic is then the one given in the
 related \texttt{semantics} paper.
 
@@ -91,8 +91,8 @@ setting.
 Nix mixes both approaches by detecting a collision between static fields at
 definition place and between dynamic fields (or between a static and a dynamic
 one) at use-time. This approach is rather inconsistent (even more if we decide
-to consider a static label $l$ as syntactic sugar for the dynamic label whose
-expression is the constant string ``$l$''), so probably will not be reflected in
+to consider a static label $s$ as syntactic sugar for the dynamic label whose
+expression is the constant string ``$s$''), so probably will not be reflected in
 the type system\footnote{It could nonethless be implemented as a pre-treatment
 of the AST in order to match nix's behaviour}.