From ab2597acf4245cff82f31fae105a8103a4b46268 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sun, 3 Feb 2019 21:19:56 +0100
Subject: Allow underscores as comments in numeral constants.

The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?
---
 doc/sphinx/language/gallina-specification-language.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

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
-- 
cgit v1.2.3