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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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