Documentation should specify what scientific notation on hexadecimal numbers means

[JasonGross]

Description of the problem

In

coq/doc/sphinx/language/core/basic.rst

Lines 114 to 134 in a12112c

	Numbers
	Numbers are sequences of digits with an optional fractional part
	and exponent, optionally preceded by a minus sign. Hexadecimal numerals
	start with ``0x`` or ``0X``. :n:`@bigint` are integers;
	numbers without fractional nor exponent parts. :n:`@bignat` are non-negative
	integers. Underscores embedded in the digits are ignored, for example
	``1_000_000`` is the same as ``1000000``.
	.. insertprodn number hexdigit
	.. prodn::
	number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat }
	| {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat }
	integer ::= {? - } @natural
	natural ::= @bignat
	bigint ::= {? - } @bignat
	bignat ::= {| @decnat | @hexnat }
	decnat ::= @digit {* {| @digit | _ } }
	digit ::= 0 .. 9
	hexnat ::= {| 0x | 0X } @hexdigit {* {| @hexdigit | _ } }
	hexdigit ::= {| 0 .. 9 | a .. f | A .. F }

There is no description of the semantics of e/E nor p/P. I know from common usage that e/E means *10^, and apparently (from experimentation) p means *2^. Both of these should be documented.

cc @proux01

Coq Version

master

[JasonGross]

@G-Sheridan yes, that seems reasonable, thanks