| Age | Commit message (Collapse) | Author |
|---|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
|
|
'e' was not displayed when printing decimal notations in R :
Require Import Reals.
Check (1.23e1, 32e+1, 0.1)%R.
was giving
< (123-1%R, 321%R, 1-1%R)
instead of
< (123e-1%R, 32e1%R, 1e-1%R)
This was introduced in #8764 (in Coq 8.10).
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2127 85f007b7-540e-0410-9357-904b9bb8a0f7
|
