5 files changed, 53 insertions, 5 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/Inductive.out b/test-suite/output/Inductive.out
index ff2556c5dc..e6c2806433 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,6 +1,10 @@
 The command has indeed failed with message:
-Last occurrence of "list'" must have "A" as 1st argument in
- "A -> list' A -> list' (A * A)%type".
+In environment
+list' : Set -> Set
+A : Set
+a : A
+l : list' A
+Unable to unify "list' (A * A)%type" with "list' A".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
 Arguments foo _%type_scope
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 4f09f00c56..bdfa8afb6a 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -4,7 +4,7 @@ fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
-proj_informative = fun '(exist _ x _) => x : A
+proj_informative = fun '(exist _ x _) => x
      : {x : A | P x} -> A
 foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
@@ -29,8 +29,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
 ∀ '(x, y), swap (x, y) = (y, x)
      : Prop
 both_z = 
-fun pat : nat * nat =>
-let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
+fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p)
      : forall pat : nat * nat, F pat
 fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop