Now that K-normalization is finished, we will proceed to optimizations, but before them we carry out α-conversion which assigns different names to different variables. This conversion is necessary because different variables with the same name would complicate various processes. For example, it translates the expression let x = 123 in let x = 456 in x + x to let x1 = 123 in let x2 = 456 in x2 + x2.
α-conversion is implemented in Alpha.g. It takes untranslated expression e with a mapping env from untranslated variable names to translated variable names, and returns the translated expression. For example, in the case of expression let x = e1 in e2, we first translate e1, create a fresh variable x', add to env the mapping from x to x', and translate e2. This process is also similar in the cases of let rec and LetTuple though they may appear more complex.
By the way, external variables are not α-converted since they are not registered in env (see function Alpha.find). This behavior is intentional: linking would not work if the names of external variables were changed.