diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/RealSyntax.out | 2 | ||||
| -rw-r--r-- | test-suite/output/RealSyntax.v | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index 2d877bd813..2b14ca7069 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,6 +2,8 @@ : R (-31)%R : R +15e-1%R + : R eq_refl : 102e-2 = 102e-2 : 102e-2 = 102e-2 eq_refl : 102e-1 = 102e-1 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index cb3bce70d4..7be8b18ac8 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -2,6 +2,8 @@ Require Import Reals.Rdefinitions. Check 32%R. Check (-31)%R. +Check 1.5_%R. + Open Scope R_scope. Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). |