GADTs augment the syntactic category constr-decls thus. The first “concrete example” of a new type is expressed as
        type _ term =
          | Int : int -> int term
          | Add : (int -> int -> int) term
          | App : ('b -> 'a) term * 'b term -> 'a term
It seems clear to me that the subtext “| Add : (int -> int -> int) term” is meant to be a constr-decl but none of the three alternative forms produce that. The alternative, new with GADTs, requires a ->.

In e-mail Jacques Garrigue suggests one more alternative to the new productions of constr-decl is needed:

| constr-name : typexpr

Bug ID = 0005875