Merge PR #12218: Numeral notations for non inductive types

Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48

1 files changed, 68 insertions, 22 deletions

diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
index 9b5c076cb4..ced52524f2 100644
--- a/test-suite/output/QArithSyntax.out
+++ b/test-suite/output/QArithSyntax.out
@@ -1,26 +1,72 @@
 eq_refl : 1.02 = 1.02
      : 1.02 = 1.02
-eq_refl : 10.2 = 10.2
-     : 10.2 = 10.2
-eq_refl : 1020 = 1020
-     : 1020 = 1020
-eq_refl : 102 = 102
-     : 102 = 102
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : -1e-4 = -1e-4
-     : -1e-4 = -1e-4
+1.02e1
+     : Q
+10.2
+     : Q
+1.02e3
+     : Q
+1020
+     : Q
+1.02e2
+     : Q
+102
+     : Q
+eq_refl : 10.2e-1 = 1.02
+     : 10.2e-1 = 1.02
+eq_refl : -0.0001 = -0.0001
+     : -0.0001 = -0.0001
 eq_refl : -0.50 = -0.50
      : -0.50 = -0.50
-eq_refl : -26 = -26
-     : -26 = -26
-eq_refl : 2860 # 256 = 2860 # 256
-     : 2860 # 256 = 2860 # 256
-eq_refl : -6882 = -6882
-     : -6882 = -6882
-eq_refl : 2860 # 64 = 2860 # 64
-     : 2860 # 64 = 2860 # 64
-eq_refl : 2860 = 2860
-     : 2860 = 2860
-eq_refl : -2860 # 1024 = -2860 # 1024
-     : -2860 # 1024 = -2860 # 1024
+0
+     : Q
+0
+     : Q
+42
+     : Q
+42
+     : Q
+1.23
+     : Q
+0x1.23%xQ
+     : Q
+0.0012
+     : Q
+42e3
+     : Q
+42e-3
+     : Q
+eq_refl : -0x1a = -0x1a
+     : -0x1a = -0x1a
+eq_refl : 0xb.2c = 0xb.2c
+     : 0xb.2c = 0xb.2c
+eq_refl : -0x1ae2 = -0x1ae2
+     : -0x1ae2 = -0x1ae2
+0xb.2cp2
+     : Q
+2860 # 64
+     : Q
+0xb.2cp8
+     : Q
+0xb2c
+     : Q
+eq_refl : -0xb.2cp-2 = -2860 # 1024
+     : -0xb.2cp-2 = -2860 # 1024
+0x0
+     : Q
+0x0
+     : Q
+0x2a
+     : Q
+0x2a
+     : Q
+1.23%Q
+     : Q
+0x1.23
+     : Q
+0x0.0012
+     : Q
+0x2ap3
+     : Q
+0x2ap-3
+     : Q