diff options
Diffstat (limited to 'doc/sphinx/language/gallina-specification-language.rst')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index bb0a9fa1bd..5a1af9f9fa 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -77,7 +77,8 @@ Identifiers and access identifiers Numerals Numerals are sequences of digits with a potential fractional part and exponent. Integers are numerals without fractional nor exponent - part and optionally preceded by a minus sign. + part and optionally preceded by a minus sign. Underscores ``_`` can + be used as comments in numerals. .. productionlist:: coq digit : 0..9 |