diff options
| author | Pierre Roux | 2019-02-03 21:19:56 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:37 +0200 |
| commit | ab2597acf4245cff82f31fae105a8103a4b46268 (patch) | |
| tree | 2ff73bd1784be5cb8d877ae51b3ccd47409a6165 /doc/sphinx | |
| parent | 6b9cb710545e1844c324979e27a04d9ddb52a924 (diff) | |
Allow underscores as comments in numeral constants.
The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?
Diffstat (limited to 'doc/sphinx')
| -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 |