From 85b3be5f6998287d90acf89de96129571b244cd7 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Jan 2020 12:43:51 +0100
Subject: Fix #11467

'e' was not displayed when printing decimal notations in R :

Require Import Reals.
Check (1.23e1, 32e+1, 0.1)%R.

was giving

< (123-1%R, 321%R, 1-1%R)

instead of

< (123e-1%R, 32e1%R, 1e-1%R)

This was introduced in #8764 (in Coq 8.10).
---
 plugins/syntax/r_syntax.ml         |  2 +-
 test-suite/output/QArithSyntax.out | 14 ++++++++++++++
 test-suite/output/QArithSyntax.v   |  9 +++++++++
 test-suite/output/RealSyntax.out   | 14 ++++++++++++++
 test-suite/output/RealSyntax.v     | 22 ++++++++++++++++++++++
 test-suite/success/QArithSyntax.v  |  9 ---------
 test-suite/success/RealSyntax.v    | 19 -------------------
 7 files changed, 60 insertions(+), 29 deletions(-)
 create mode 100644 test-suite/output/QArithSyntax.out
 create mode 100644 test-suite/output/QArithSyntax.v
 delete mode 100644 test-suite/success/QArithSyntax.v
 delete mode 100644 test-suite/success/RealSyntax.v

diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 70c1077106..f6fbdaa958 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -164,7 +164,7 @@ let rawnum_of_r c = match DAst.get c with
              let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in
              let i = Bigint.to_string i in
              let se = if is_gr md glob_Rdiv then "-" else "" in
-             let e = se ^ Bigint.to_string e in
+             let e = "e" ^ se ^ Bigint.to_string e in
              s, { NumTok.int = i; frac = ""; exp = e }
         | _ -> raise Non_closed_number
         end
diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
new file mode 100644
index 0000000000..6bc04f1cef
--- /dev/null
+++ b/test-suite/output/QArithSyntax.out
@@ -0,0 +1,14 @@
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : 102e-1 = 102e-1
+     : 102e-1 = 102e-1
+eq_refl : 1020 = 1020
+     : 1020 = 1020
+eq_refl : 102 = 102
+     : 102 = 102
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : -1e-4 = -1e-4
+     : -1e-4 = -1e-4
+eq_refl : -50e-2 = -50e-2
+     : -50e-2 = -50e-2
diff --git a/test-suite/output/QArithSyntax.v b/test-suite/output/QArithSyntax.v
new file mode 100644
index 0000000000..2f2ee0134a
--- /dev/null
+++ b/test-suite/output/QArithSyntax.v
@@ -0,0 +1,9 @@
+Require Import QArith.
+Open Scope Q_scope.
+Check (eq_refl : 1.02 = 102 # 100).
+Check (eq_refl : 1.02e1 = 102 # 10).
+Check (eq_refl : 1.02e+03 = 1020).
+Check (eq_refl : 1.02e+02 = 102 # 1).
+Check (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = -1 # 10000).
+Check (eq_refl : -0.50 = - 50 # 100).
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index e6f7556d96..2d877bd813 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -2,3 +2,17 @@
      : R
 (-31)%R
      : R
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : 102e-1 = 102e-1
+     : 102e-1 = 102e-1
+eq_refl : 102e1 = 102e1
+     : 102e1 = 102e1
+eq_refl : 102 = 102
+     : 102 = 102
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : -1e-4 = -1e-4
+     : -1e-4 = -1e-4
+eq_refl : -50e-2 = -50e-2
+     : -50e-2 = -50e-2
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 44e8c7a50c..cb3bce70d4 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -1,3 +1,25 @@
 Require Import Reals.Rdefinitions.
 Check 32%R.
 Check (-31)%R.
+
+Open Scope R_scope.
+
+Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
+Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+02 = IZR 102).
+Check (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
+Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)).
+
+Require Import Reals.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+ring.
+Qed.
+
+Require Import Psatz.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+lra.
+Qed.
diff --git a/test-suite/success/QArithSyntax.v b/test-suite/success/QArithSyntax.v
deleted file mode 100644
index 2f2ee0134a..0000000000
--- a/test-suite/success/QArithSyntax.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import QArith.
-Open Scope Q_scope.
-Check (eq_refl : 1.02 = 102 # 100).
-Check (eq_refl : 1.02e1 = 102 # 10).
-Check (eq_refl : 1.02e+03 = 1020).
-Check (eq_refl : 1.02e+02 = 102 # 1).
-Check (eq_refl : 10.2e-1 = 1.02).
-Check (eq_refl : -0.0001 = -1 # 10000).
-Check (eq_refl : -0.50 = - 50 # 100).
diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v
deleted file mode 100644
index 2765200991..0000000000
--- a/test-suite/success/RealSyntax.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import Reals.
-Open Scope R_scope.
-Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
-Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+02 = IZR 102).
-Check (eq_refl : 10.2e-1 = 1.02).
-Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
-Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)).
-
-Goal 254e3 = 2540 * 10 ^ 2.
-ring.
-Qed.
-
-Require Import Psatz.
-
-Goal 254e3 = 2540 * 10 ^ 2.
-lra.
-Qed.
-- 
cgit v1.2.3