From ed399336b886a062e0e3070314c117d62d9a8af3 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Wed, 18 Mar 2020 21:33:34 +0100
Subject: Print a warning when parsing non floating-point values.

For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
---
 test-suite/output/FloatSyntax.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'test-suite/output/FloatSyntax.v')

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.
-- 
cgit v1.2.3