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).

1 files changed, 1 insertions, 1 deletions

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