From ec2f7507daaa5d3fa7ba365e542351457a237f43 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Mar 2020 23:12:28 +0100
Subject: Fixing little bug in parsing decimal numbers in R.

---
 test-suite/output/RealSyntax.out | 2 ++
 test-suite/output/RealSyntax.v   | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'test-suite')

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