aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorArmael2018-03-13 17:16:55 +0100
committerArmael2018-03-13 17:33:52 +0100
commite31fa0ecb1f823cc5735fa63330f430e2c0d96e2 (patch)
treea203fe5b711daafb59d41799e5161b215c89c7de /doc
parent797cd88b4ea91780fca394a12044f9613ed63fc6 (diff)
Fix another typo in the documentation's grammar for open variants
Diffstat (limited to 'doc')
-rw-r--r--doc/ltac2.md2
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₀ ")" )