10 files changed, 233 insertions, 17 deletions
diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
index cfd6633752..dd8189c56f 100644
--- a/test-suite/output/FloatExtraction.out
+++ b/test-suite/output/FloatExtraction.out
@@ -1,3 +1,17 @@
+File "stdin", line 25, characters 8-12:
+Warning: The constant 0.01 is not a binary64 floating-point value. A closest
+value will be used and unambiguously printed 0.01. [inexact-float,parsing]
+File "stdin", line 25, characters 20-25:
+Warning: The constant -0.01 is not a binary64 floating-point value. A closest
+value will be used and unambiguously printed -0.01. [inexact-float,parsing]
+File "stdin", line 25, characters 27-35:
+Warning: The constant 1.7e+308 is not a binary64 floating-point value. A
+closest value will be used and unambiguously printed 1.6999999999999999e+308.
+[inexact-float,parsing]
+File "stdin", line 25, characters 37-46:
+Warning: The constant -1.7e-308 is not a binary64 floating-point value. A
+closest value will be used and unambiguously printed
+-1.7000000000000002e-308. [inexact-float,parsing]
 
 (** val infinity : Float64.t **)
 
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
index 668a55977d..7941d2e647 100644
--- a/test-suite/output/FloatSyntax.out
+++ b/test-suite/output/FloatSyntax.out
@@ -4,8 +4,16 @@
      : float
 (-2.5)%float
      : float
+File "stdin", line 9, characters 6-13:
+Warning: The constant 2.5e123 is not a binary64 floating-point value. A
+closest value will be used and unambiguously printed 2.4999999999999999e+123.
+[inexact-float,parsing]
 2.4999999999999999e+123%float
      : float
+File "stdin", line 10, characters 7-16:
+Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
+closest value will be used and unambiguously printed
+-2.5000000000000001e-123. [inexact-float,parsing]
 (-2.5000000000000001e-123)%float
      : float
 (2 + 2)%float
@@ -18,14 +26,34 @@
      : float
 -2.5
      : float
+File "stdin", line 19, characters 6-13:
+Warning: The constant 2.5e123 is not a binary64 floating-point value. A
+closest value will be used and unambiguously printed 2.4999999999999999e+123.
+[inexact-float,parsing]
 2.4999999999999999e+123
      : float
+File "stdin", line 20, characters 7-16:
+Warning: The constant -2.5e-123 is not a binary64 floating-point value. A
+closest value will be used and unambiguously printed
+-2.5000000000000001e-123. [inexact-float,parsing]
 -2.5000000000000001e-123
      : float
 2 + 2
      : float
 2.5 + 2.5
      : float
+File "stdin", line 24, characters 6-11:
+Warning: The constant 1e309 is not a binary64 floating-point value. A closest
+value will be used and unambiguously printed infinity.
+[inexact-float,parsing]
+infinity
+     : float
+File "stdin", line 25, characters 6-12:
+Warning: The constant -1e309 is not a binary64 floating-point value. A
+closest value will be used and unambiguously printed neg_infinity.
+[inexact-float,parsing]
+neg_infinity
+     : float
 2
      : nat
 2%float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
index 85f611352c..eca712db10 100644
--- a/test-suite/output/FloatSyntax.v
+++ b/test-suite/output/FloatSyntax.v
@@ -21,6 +21,9 @@ Check (-2.5e-123).
 Check (2 + 2).
 Check (2.5 + 2.5).
 
+Check 1e309.
+Check -1e309.
+
 Open Scope nat_scope.
 
 Check 2.
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 113384e9cf..060877707b 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -218,3 +218,19 @@ let v : ty := Build_ty Set set in v : ty
      : ty
 let v : ty := Build_ty Type type in v : ty
      : ty
+1
+     : nat
+(-1000)%Z
+     : Z
+0
+     : Prop
++0
+     : bool
+-0
+     : bool
+00
+     : nat * nat
+1000
+     : Prop
+1_000
+     : list nat
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 22aff36d67..47e1b127cb 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -457,3 +457,33 @@ Module Test20.
   Check let v := 4%kt in v : ty.
   Check let v := 5%kt in v : ty.
 End Test20.
+
+Module Test21.
+
+  Check 00001.
+  Check (-1_000)%Z.
+
+End Test21.
+
+Module Test22.
+
+Notation "0" := False.
+Notation "+0" := true.
+Notation "-0" := false.
+Notation "00" := (0%nat, 0%nat).
+Check 0.
+Check +0.
+Check -0.
+Check 00.
+
+Notation "1000" := True.
+Notation "1_000" := (cons 1 nil).
+Check 1000.
+Check 1_000.
+
+(* To do: preserve parsing of -0:
+Require Import ZArith.
+Check (-0)%Z.
+*)
+
+End Test22.
diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
index 6bc04f1cef..fe6a1d25c6 100644
--- a/test-suite/output/QArithSyntax.out
+++ b/test-suite/output/QArithSyntax.out
@@ -1,14 +1,14 @@
-eq_refl : 102e-2 = 102e-2
-     : 102e-2 = 102e-2
-eq_refl : 102e-1 = 102e-1
-     : 102e-1 = 102e-1
+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 : 102e-2 = 102e-2
-     : 102e-2 = 102e-2
+eq_refl : 1.02 = 1.02
+     : 1.02 = 1.02
 eq_refl : -1e-4 = -1e-4
      : -1e-4 = -1e-4
-eq_refl : -50e-2 = -50e-2
-     : -50e-2 = -50e-2
+eq_refl : -0.50 = -0.50
+     : -0.50 = -0.50
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index 2b14ca7069..1685964b0f 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -2,19 +2,21 @@
      : R
 (-31)%R
      : R
-15e-1%R
+1.5%R
      : R
-eq_refl : 102e-2 = 102e-2
-     : 102e-2 = 102e-2
-eq_refl : 102e-1 = 102e-1
-     : 102e-1 = 102e-1
+15%R
+     : R
+eq_refl : 1.02 = 1.02
+     : 1.02 = 1.02
+eq_refl : 10.2 = 10.2
+     : 10.2 = 10.2
 eq_refl : 102e1 = 102e1
      : 102e1 = 102e1
 eq_refl : 102 = 102
      : 102 = 102
-eq_refl : 102e-2 = 102e-2
-     : 102e-2 = 102e-2
+eq_refl : 1.02 = 1.02
+     : 1.02 = 1.02
 eq_refl : -1e-4 = -1e-4
      : -1e-4 = -1e-4
-eq_refl : -50e-2 = -50e-2
-     : -50e-2 = -50e-2
+eq_refl : -0.50 = -0.50
+     : -0.50 = -0.50
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 7be8b18ac8..e5f9d06316 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -3,6 +3,7 @@ Check 32%R.
 Check (-31)%R.
 
 Check 1.5_%R.
+Check 1_.5_e1_%R.
 
 Open Scope R_scope.
 
diff --git a/test-suite/output/allBytes.out b/test-suite/output/allBytes.out
new file mode 100644
index 0000000000..8d188c4c45
--- /dev/null
+++ b/test-suite/output/allBytes.out
@@ -0,0 +1 @@
+!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~
diff --git a/test-suite/output/allBytes.v b/test-suite/output/allBytes.v
new file mode 100644
index 0000000000..01a5161ef4
--- /dev/null
+++ b/test-suite/output/allBytes.v
@@ -0,0 +1,121 @@
+(* Taken from bedrock2 *)
+
+(* Note: not an utf8 file *)
+
+Require Import Coq.ZArith.BinInt Coq.Lists.List.
+Require Coq.Init.Byte Coq.Strings.Byte Coq.Strings.String.
+
+Definition allBytes: list Byte.byte :=
+  map (fun nn => match Byte.of_N (BinNat.N.of_nat nn) with
+                 | Some b => b
+                 | None => Byte.x00 (* won't happen *)
+                 end)
+      (seq 32 95).
+
+Notation "a b" := (@cons Byte.byte a b)
+  (only printing, right associativity, at level 3, format "a b").
+
+Notation "" := (@nil Byte.byte)
+  (only printing, right associativity, at level 3, format "").
+
+Notation "  " := (Byte.x20) (only printing).
+Notation "'!'" := (Byte.x21) (only printing).
+Notation "'""'" := (Byte.x22) (only printing).
+Notation "'#'" := (Byte.x23) (only printing).
+Notation "'$'" := (Byte.x24) (only printing).
+Notation "'%'" := (Byte.x25) (only printing).
+Notation "'&'" := (Byte.x26) (only printing).
+Notation "'''" := (Byte.x27) (only printing).
+Notation "'('" := (Byte.x28) (only printing).
+Notation "')'" := (Byte.x29) (only printing).
+Notation "'*'" := (Byte.x2a) (only printing).
+Notation "'+'" := (Byte.x2b) (only printing).
+Notation "','" := (Byte.x2c) (only printing).
+Notation "'-'" := (Byte.x2d) (only printing).
+Notation "'.'" := (Byte.x2e) (only printing).
+Notation "'/'" := (Byte.x2f) (only printing).
+Notation "'0'" := (Byte.x30) (only printing).
+Notation "'1'" := (Byte.x31) (only printing).
+Notation "'2'" := (Byte.x32) (only printing).
+Notation "'3'" := (Byte.x33) (only printing).
+Notation "'4'" := (Byte.x34) (only printing).
+Notation "'5'" := (Byte.x35) (only printing).
+Notation "'6'" := (Byte.x36) (only printing).
+Notation "'7'" := (Byte.x37) (only printing).
+Notation "'8'" := (Byte.x38) (only printing).
+Notation "'9'" := (Byte.x39) (only printing).
+Notation "':'" := (Byte.x3a) (only printing).
+Notation "';'" := (Byte.x3b) (only printing).
+Notation "'<'" := (Byte.x3c) (only printing).
+Notation "'='" := (Byte.x3d) (only printing).
+Notation "'>'" := (Byte.x3e) (only printing).
+Notation "'?'" := (Byte.x3f) (only printing).
+Notation "'@'" := (Byte.x40) (only printing).
+Notation "'A'" := (Byte.x41) (only printing).
+Notation "'B'" := (Byte.x42) (only printing).
+Notation "'C'" := (Byte.x43) (only printing).
+Notation "'D'" := (Byte.x44) (only printing).
+Notation "'E'" := (Byte.x45) (only printing).
+Notation "'F'" := (Byte.x46) (only printing).
+Notation "'G'" := (Byte.x47) (only printing).
+Notation "'H'" := (Byte.x48) (only printing).
+Notation "'I'" := (Byte.x49) (only printing).
+Notation "'J'" := (Byte.x4a) (only printing).
+Notation "'K'" := (Byte.x4b) (only printing).
+Notation "'L'" := (Byte.x4c) (only printing).
+Notation "'M'" := (Byte.x4d) (only printing).
+Notation "'N'" := (Byte.x4e) (only printing).
+Notation "'O'" := (Byte.x4f) (only printing).
+Notation "'P'" := (Byte.x50) (only printing).
+Notation "'Q'" := (Byte.x51) (only printing).
+Notation "'R'" := (Byte.x52) (only printing).
+Notation "'S'" := (Byte.x53) (only printing).
+Notation "'T'" := (Byte.x54) (only printing).
+Notation "'U'" := (Byte.x55) (only printing).
+Notation "'V'" := (Byte.x56) (only printing).
+Notation "'W'" := (Byte.x57) (only printing).
+Notation "'X'" := (Byte.x58) (only printing).
+Notation "'Y'" := (Byte.x59) (only printing).
+Notation "'Z'" := (Byte.x5a) (only printing).
+Notation "'['" := (Byte.x5b) (only printing).
+Notation "'\'" := (Byte.x5c) (only printing).
+Notation "']'" := (Byte.x5d) (only printing).
+Notation "'^'" := (Byte.x5e) (only printing).
+Notation "'_'" := (Byte.x5f) (only printing).
+Notation "'`'" := (Byte.x60) (only printing).
+Notation "'a'" := (Byte.x61) (only printing).
+Notation "'b'" := (Byte.x62) (only printing).
+Notation "'c'" := (Byte.x63) (only printing).
+Notation "'d'" := (Byte.x64) (only printing).
+Notation "'e'" := (Byte.x65) (only printing).
+Notation "'f'" := (Byte.x66) (only printing).
+Notation "'g'" := (Byte.x67) (only printing).
+Notation "'h'" := (Byte.x68) (only printing).
+Notation "'i'" := (Byte.x69) (only printing).
+Notation "'j'" := (Byte.x6a) (only printing).
+Notation "'k'" := (Byte.x6b) (only printing).
+Notation "'l'" := (Byte.x6c) (only printing).
+Notation "'m'" := (Byte.x6d) (only printing).
+Notation "'n'" := (Byte.x6e) (only printing).
+Notation "'o'" := (Byte.x6f) (only printing).
+Notation "'p'" := (Byte.x70) (only printing).
+Notation "'q'" := (Byte.x71) (only printing).
+Notation "'r'" := (Byte.x72) (only printing).
+Notation "'s'" := (Byte.x73) (only printing).
+Notation "'t'" := (Byte.x74) (only printing).
+Notation "'u'" := (Byte.x75) (only printing).
+Notation "'v'" := (Byte.x76) (only printing).
+Notation "'w'" := (Byte.x77) (only printing).
+Notation "'x'" := (Byte.x78) (only printing).
+Notation "'y'" := (Byte.x79) (only printing).
+Notation "'z'" := (Byte.x7a) (only printing).
+Notation "'{'" := (Byte.x7b) (only printing).
+Notation "'|'" := (Byte.x7c) (only printing).
+Notation "'}'" := (Byte.x7d) (only printing).
+Notation "'~'" := (Byte.x7e) (only printing).
+
+Global Set Printing Width 300.
+
+Goal False.
+  let cc := eval cbv in allBytes in idtac cc.
+Abort.