The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

>  I believe the documentation is incorrect and should not include that syntax.

No, the grammar is correct.  It's not a syntax error at all (Ex: "Syntax error: illegal begin of vernac."), it's a semantic restriction, which should be documented.

Note that "pattern" is not just used in match, it's also used in let-in definitions: https://coq.inria.fr/refman/language/core/definitions.html#let-in-definitions.

The source code says this about the message:

(* We raise an error if the pattern contains a cast, due to
   current restrictions on casts in patterns. Cast in patterns
   are supported only in local binders and only at top level.
   The only reason they are in the [cases_pattern_expr] type
   is that the parser needs to factor the "c : t" notation
   with user defined notations. In the long term, we will try to
   support such casts everywhere, and perhaps use them to print
   the domains of lambdas in the encoding of match in constr.
   This check is here and not in the parser because it would require

   duplicating the levels of the [pattern] rule. *)

Jim