Syntax rule for dependent function types

[AxelBoldt]

Section 1.4 contains the sentence "Like λ-abstractions, Πs automatically scope over the rest of
the expression unless delimited", but it should occur earlier, since the issue already arises three paragraphs earlier, in the discussion of the polymorphic identity function.

[andrejbauer]

Should this have been closed by @mikeshulman commit above?

[mikeshulman]

Someone needs to merge #951 first.