In the preceding chapters, we presented a few elements of type synthesis in CAML. Chapter 5 gave you a description that was almost complete, with the exception of how to manage polymorphism. In effect, Section 5.3.1 informally showed you constraints that must be respected for a program to be typable. Since CAML has a polymorphic type system, a value like e1 introduced by let x = e1 in e2 may have different types, even types that are incompatible with one another, at every occurrence of x in e2.
However, in Section 5.3.1, we suggested that the same effect could be achieved by typing the expression e2 in which we substitute the expression e1 for the free occurrences of x, that is, e2 [x ← e1] in place of let x