type-expr is defined twice

[signoles]

Grammar entry "type-expr" is defined twice in incompatible ways: once in Fig. 2.4 (Grammar of binders and type expression) and once in Fig. 2.14 (Grammar for global logic definitions).

[vprevosto]

This might not be the best presentation, but this is meant to be additive: figure 2.4 deals with plain type, while 2.14 adds new possibilities when dealing with polymorphism. This appears for other entries as well. For instance term in figure 2.1 does not contain \at, which is only introduced in figure 2.12

[signoles]

Adding ... or any other recognizable pattern in the first line of a declaration that extends an existing grammar rule would be clearer IMHO.