aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index fe359a23a9..f4592f8f37 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -117,7 +117,7 @@ Other tokens
! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
. .( .. ... / : ::= := :> :>> ; < <+ <- <:
- <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn
+ <<: <= = => > >-> >= ? @ @{ [ [= ] _
`( `{ { {| | |- || }
When multiple tokens match the beginning of a sequence of characters,