diff options
| author | Pierre Roux | 2020-01-28 12:43:51 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-01-28 22:19:27 +0100 |
| commit | 85b3be5f6998287d90acf89de96129571b244cd7 (patch) | |
| tree | 97d8f65bb143e2d69d449857fe2cc1ed5422f8e6 /test-suite/output/RealSyntax.v | |
| parent | 614643e6fb1b5029d1c2bf50cd51f95d621010cf (diff) | |
Fix #11467
'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).
Diffstat (limited to 'test-suite/output/RealSyntax.v')
| -rw-r--r-- | test-suite/output/RealSyntax.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 44e8c7a50c..cb3bce70d4 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -1,3 +1,25 @@ Require Import Reals.Rdefinitions. Check 32%R. Check (-31)%R. + +Open Scope R_scope. + +Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). +Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+02 = IZR 102). +Check (eq_refl : 10.2e-1 = 1.02). +Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). +Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). + +Require Import Reals. + +Goal 254e3 = 2540 * 10 ^ 2. +ring. +Qed. + +Require Import Psatz. + +Goal 254e3 = 2540 * 10 ^ 2. +lra. +Qed. |