diff options
| -rw-r--r-- | doc/ltac2.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/ltac2.md b/doc/ltac2.md index 10a65fce44..9ba227c285 100644 --- a/doc/ltac2.md +++ b/doc/ltac2.md @@ -127,7 +127,7 @@ TYPEDEF := | TYPE | "[" CONSTRUCTORDEF₀ "|" ... "|" CONSTRUCTORDEFₙ "]" | "{" FIELDDEF₀ ";" ... ";" FIELDDEFₙ "}" -| "[" "..." "]" +| "[" ".." "]" CONSTRUCTORDEF := | IDENT ( "(" TYPE₀ "," ... "," TYPE₀ ")" ) |