语法错误：“。”当对整数使用归纳时，在 Coq 中预期在 [vernac:gallina]（在 [vernac_aux] 中）之后

Question

所以我试图在 coq 中定义一个从 0 到 10 的整数的归纳集：

Inductive OD : Set := 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10.

我收到这条消息：

Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).

我试过的都没有真正奏效