[numeral notation] R

Previously real constants were parsed by an unproved OCaml code. The
parser and printer are now implemented in Coq, which will enable a
proof and hopefully make it easier to maintain / make evolve.

Previously reals were all parsed as an integer, an integer multiplied
by a power of ten or an integer divided by a power of ten. This means
1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell
apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.

Now, decimal dot is parsed as a rational and exponents are parsed as a
product or division by a power of ten. For instance, 1.02 is parsed as
Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos
10 2).

1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R
(102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.

11 files changed, 266 insertions, 273 deletions

diff --git a/Makefile.common b/Makefile.common
index a482b9b963..29020dc4ad 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -149,7 +149,6 @@ CCCMO:=plugins/cc/cc_plugin.cmo
 BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo
 RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
 SYNTAXCMO:=$(addprefix plugins/syntax/, \
-        r_syntax_plugin.cmo \
 	int63_syntax_plugin.cmo \
 	float_syntax_plugin.cmo \
 	numeral_notation_plugin.cmo \
diff --git a/plugins/syntax/dune b/plugins/syntax/dune
index b395695c8a..1b3d7598da 100644
--- a/plugins/syntax/dune
+++ b/plugins/syntax/dune
@@ -13,13 +13,6 @@
  (libraries coq.vernac))
 
 (library
- (name r_syntax_plugin)
- (public_name coq.plugins.r_syntax)
- (synopsis "Coq syntax plugin: reals")
- (modules r_syntax)
- (libraries coq.vernac))
-
-(library
  (name int63_syntax_plugin)
  (public_name coq.plugins.int63_syntax)
  (synopsis "Coq syntax plugin: int63")
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
deleted file mode 100644
index d66b9537b4..0000000000
--- a/plugins/syntax/r_syntax.ml
+++ /dev/null
@@ -1,214 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Names
-open Glob_term
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "r_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-exception Non_closed_number
-
-(**********************************************************************)
-(* Parsing positive via scopes                                        *)
-(**********************************************************************)
-
-let binnums = ["Coq";"Numbers";"BinNums"]
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let positive_modpath = MPfile (make_dir binnums)
-
-let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
-let path_of_xI = ((positive_kn,0),1)
-let path_of_xO = ((positive_kn,0),2)
-let path_of_xH = ((positive_kn,0),3)
-let glob_xI = GlobRef.ConstructRef path_of_xI
-let glob_xO = GlobRef.ConstructRef path_of_xO
-let glob_xH = GlobRef.ConstructRef path_of_xH
-
-let pos_of_bignat ?loc x =
-  let ref_xI = DAst.make @@ GRef (glob_xI, None) in
-  let ref_xH = DAst.make @@ GRef (glob_xH, None) in
-  let ref_xO = DAst.make @@ GRef (glob_xO, None) in
-  let rec pos_of x =
-    match Z.(div_rem x (of_int 2)) with
-      | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q])
-      | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
-      | (q,_) -> ref_xH
-  in
-  pos_of x
-
-(**********************************************************************)
-(* Printing positive via scopes                                       *)
-(**********************************************************************)
-
-let rec bignat_of_pos c = match DAst.get c with
-  | GApp (r, [a]) when is_gr r glob_xO -> Z.mul Z.(of_int 2) (bignat_of_pos a)
-  | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a))
-  | GRef (a, _) when GlobRef.equal a glob_xH -> Z.one
-  | _ -> raise Non_closed_number
-
-(**********************************************************************)
-(* Parsing Z via scopes                                               *)
-(**********************************************************************)
-
-let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
-let path_of_ZERO = ((z_kn,0),1)
-let path_of_POS = ((z_kn,0),2)
-let path_of_NEG = ((z_kn,0),3)
-let glob_ZERO = GlobRef.ConstructRef path_of_ZERO
-let glob_POS = GlobRef.ConstructRef path_of_POS
-let glob_NEG = GlobRef.ConstructRef path_of_NEG
-
-let z_of_int ?loc n =
-  if not Z.(equal n zero) then
-    let sgn, n =
-      if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.neg n in
-    DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
-  else
-    DAst.make @@ GRef (glob_ZERO, None)
-
-(**********************************************************************)
-(* Printing Z via scopes                                              *)
-(**********************************************************************)
-
-let bigint_of_z c = match DAst.get c with
-  | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
-  | GApp (r,[a]) when is_gr r glob_NEG -> Z.neg (bignat_of_pos a)
-  | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero
-  | _ -> raise Non_closed_number
-
-(**********************************************************************)
-(* Parsing R via scopes                                               *)
-(**********************************************************************)
-
-let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
-let r_modpath = MPfile (make_dir rdefinitions)
-let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl")
-let r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R"
-
-let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
-let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult")
-let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv")
-
-let binintdef = ["Coq";"ZArith";"BinIntDef"]
-let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z")
-
-let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos")
-
-let r_of_rawnum ?loc n =
-  let n,e = NumTok.Signed.to_bigint_and_exponent n in
-  let e,p = NumTok.(match e with EDec e -> e, 10 | EBin e -> e, 2) in
-  let izr z =
-    DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in
-  let rmult r r' =
-    DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in
-  let rdiv r r' =
-    DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in
-  let pow p e =
-    let p = z_of_int ?loc (Z.of_int p) in
-    let e = pos_of_bignat e in
-    DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in
-  let n =
-    izr (z_of_int ?loc n) in
-  if Int.equal (Z.sign e) 1 then rmult n (izr (pow p e))
-  else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e)))
-  else n  (* e = 0 *)
-
-(**********************************************************************)
-(* Printing R via scopes                                              *)
-(**********************************************************************)
-
-let rawnum_of_r c =
-  (* print i * 10^e, precondition: e <> 0 *)
-  let numTok_of_int_exp i e =
-    (* choose between 123e-2 and 1.23, this is purely heuristic
-       and doesn't play any soundness role *)
-    let choose_exponent =
-      if Int.equal (Z.sign e) 1 then
-        true  (* don't print 12 * 10^2 as 1200 to distinguish them *)
-      else
-        let i = Z.to_string i in
-        let li = if i.[0] = '-' then String.length i - 1 else String.length i in
-        let e = Z.neg e in
-        let le = String.length (Z.to_string e) in
-        Z.(lt (add (of_int li) (of_int le)) e) in
-    (* print 123 * 10^-2 as 123e-2 *)
-    let numTok_exponent () =
-      NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in
-    (* print 123 * 10^-2 as 1.23, precondition e < 0 *)
-    let numTok_dot () =
-      let s, i =
-        if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i
-        else NumTok.SMinus, Z.(to_string (neg i)) in
-      let ni = String.length i in
-      let e = - (Z.to_int e) in
-      assert (e > 0);
-      let i, f =
-        if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e
-        else "0", String.make (e - ni) '0' ^ i in
-      let i = s, NumTok.UnsignedNat.of_string i in
-      let f = NumTok.UnsignedNat.of_string f in
-      NumTok.Signed.of_int_frac_and_exponent i (Some f) None in
-    if choose_exponent then numTok_exponent () else numTok_dot () in
-  match DAst.get c with
-  | GApp (r, [a]) when is_gr r glob_IZR ->
-     let n = bigint_of_z a in
-     NumTok.(Signed.of_bigint CDec n)
-  | GApp (md,  [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv ->
-     begin match DAst.get l, DAst.get r with
-     | GApp (i, [l]), GApp (i', [r])
-          when is_gr i glob_IZR && is_gr i' glob_IZR ->
-        begin match DAst.get r with
-        | GApp (p, [t; e]) when is_gr p glob_pow_pos ->
-           let t = bigint_of_z t in
-           if not (Z.(equal t (of_int 10))) then
-             raise Non_closed_number
-           else
-             let i = bigint_of_z l in
-             let e = bignat_of_pos e in
-             let e = if is_gr md glob_Rdiv then Z.neg e else e in
-             numTok_of_int_exp i e
-        | _ -> raise Non_closed_number
-        end
-     | _ -> raise Non_closed_number
-     end
-  | _ -> raise Non_closed_number
-
-let uninterp_r (AnyGlobConstr p) =
-  try
-    Some (rawnum_of_r p)
-  with Non_closed_number ->
-    None
-
-open Notation
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let r_scope = "R_scope"
-
-let _ =
-  register_rawnumeral_interpretation r_scope (r_of_rawnum,uninterp_r);
-  at_declare_ml_module enable_prim_token_interpretation
-    { pt_local = false;
-      pt_scope = r_scope;
-      pt_interp_info = Uid r_scope;
-      pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
-      pt_refs = [glob_IZR; glob_Rmult; glob_Rdiv];
-      pt_in_match = false }
diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli
deleted file mode 100644
index b72d544151..0000000000
--- a/plugins/syntax/r_syntax.mli
+++ /dev/null
@@ -1,9 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack
deleted file mode 100644
index d4ee75ea48..0000000000
--- a/plugins/syntax/r_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-R_syntax
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index a9386b2781..a7b7dabb20 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -4,34 +4,81 @@
      : R
 1.5%R
      : R
-15%R
-     : R
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : 10.2 = 10.2
-     : 10.2 = 10.2
-eq_refl : 102e1 = 102e1
-     : 102e1 = 102e1
-eq_refl : 102 = 102
-     : 102 = 102
-eq_refl : 1.02 = 1.02
-     : 1.02 = 1.02
-eq_refl : -1e-4 = -1e-4
-     : -1e-4 = -1e-4
-eq_refl : -0.50 = -0.50
-     : -0.50 = -0.50
+1.5e1%R
+     : R
+eq_refl : 1.02 = 102e-2
+     : 1.02 = 102e-2
+1.02e1
+     : R
+102e-1
+     : R
+1.02e3
+     : R
+102e1
+     : R
+1.02e2
+     : R
+102
+     : R
+10.2e-1
+     : R
+1.02
+     : R
+eq_refl : -0.0001 = -1e-4
+     : -0.0001 = -1e-4
+eq_refl : -0.50 = -50e-2
+     : -0.50 = -50e-2
 eq_refl : -26 = -26
      : -26 = -26
-eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8)
-     : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8)
+eq_refl : 0xb.2c%xR = 0xb2cp-8%xR
+     : 0xb.2c%xR = 0xb2cp-8%xR
 eq_refl : -6882 = -6882
      : -6882 = -6882
-eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6)
-     : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6)
-eq_refl : 2860 = 2860
-     : 2860 = 2860
-eq_refl
-:
--2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - (2860) / IZR (Z.pow_pos 2 10)
-     : -2860 / IZR (BinIntDef.Z.pow_pos 2 10) =
-       - (2860) / IZR (Z.pow_pos 2 10)
+0xb.2cp2%xR
+     : R
+0xb2cp-6%xR
+     : R
+0xb.2cp8%xR
+     : R
+2860
+     : R
+(-0xb.2cp-2)%xR
+     : R
+- 0xb2cp-10%xR
+     : R
+0
+     : R
+0
+     : R
+42
+     : R
+42
+     : R
+1.23
+     : R
+0x1.23%xR
+     : R
+0.0012
+     : R
+42e3
+     : R
+42e-3
+     : R
+0x0
+     : R
+0x0
+     : R
+0x2a
+     : R
+0x2a
+     : R
+1.23%R
+     : R
+0x1.23
+     : R
+0x0.0012
+     : R
+0x2ap3
+     : R
+0x2ap-3
+     : R
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 69ce3ef5f9..790d5c654f 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -8,18 +8,48 @@ Check 1_.5_e1_%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 1.02e1.
+Check IZR 102 / IZR (Z.pow_pos 10 1).
+Check 1.02e+03.
+Check IZR 102 * IZR (Z.pow_pos 10 1).
+Check 1.02e+02.
+Check IZR 102.
+Check 10.2e-1.
+Check 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)).
 Check (eq_refl : -0x1a = - 26).
 Check (eq_refl : 0xb.2c = IZR 2860 / IZR (Z.pow_pos 2 8)).
 Check (eq_refl : -0x1ae2 = -6882).
-Check (eq_refl : 0xb.2cp2 = IZR 2860 / IZR (Z.pow_pos 2 6)).
-Check (eq_refl : 0xb.2cp8 = 2860).
-Check (eq_refl : -0xb.2cp-2 = - IZR 2860 / IZR (Z.pow_pos 2 10)).
+Check 0xb.2cp2.
+Check IZR 2860 / IZR (Z.pow_pos 2 6).
+Check 0xb.2cp8.
+Check 2860.
+Check -0xb.2cp-2.
+Check - (IZR 2860 / IZR (Z.pow_pos 2 10)).
+Check 0.
+Check 000.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0.0012.
+Check 42e3.
+Check 42e-3.
+
+Open Scope hex_R_scope.
+
+Check 0x0.
+Check 0x000.
+Check 42.
+Check 0x2a.
+Check 1.23.
+Check 0x1.23.
+Check 0x0.0012.
+Check 0x2ap3.
+Check 0x2ap-3.
+
+Close Scope hex_R_scope.
 
 Require Import Reals.
 
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 1baefd6bf7..20b5cb236b 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -13,8 +13,6 @@ Require Export QArith_base.
 
 (** Injection of rational numbers into real numbers. *)
 
-Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
-
 Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R.
 Proof.
 intros.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index affa129771..a4809a7513 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -22,11 +22,12 @@ Require Import ConstructiveRcomplete.
 Require Import ClassicalDedekindReals.
 
 
-(* Declare primitive numeral notations for Scope R_scope *)
+(* Declare primitive number notations for Scope R_scope *)
+Declare Scope hex_R_scope.
 Declare Scope R_scope.
-Declare ML Module "r_syntax_plugin".
 
 (* Declare Scope R_scope with Key R *)
+Delimit Scope hex_R_scope with xR.
 Delimit Scope R_scope with R.
 
 Local Open Scope R_scope.
@@ -224,3 +225,153 @@ Proof.
   - (* x = n-1 *) exact n.
   - exact (Z.pred n).
 Defined.
+
+(** Injection of rational numbers into real numbers. *)
+
+Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
+
+(**********************************************************)
+(** *    Number notation for constants                    *)
+(**********************************************************)
+
+Inductive IR :=
+  | IRZ : IZ -> IR
+  | IRQ : Q -> IR
+  | IRmult : IR -> IR -> IR
+  | IRdiv : IR -> IR -> IR.
+
+Definition of_decimal (d : Decimal.decimal) : IR :=
+  let '(i, f, e) :=
+    match d with
+    | Decimal.Decimal i f => (i, f, Decimal.Pos Decimal.Nil)
+    | Decimal.DecimalExp i f e => (i, f, e)
+    end in
+  let zq := match f with
+    | Decimal.Nil => IRZ (IZ_of_Z (Z.of_int i))
+    | _ =>
+      let num := Z.of_int (Decimal.app_int i f) in
+      let den := Nat.iter (Decimal.nb_digits f) (Pos.mul 10) 1%positive in
+      IRQ (Qmake num den) end in
+  let e := Z.of_int e in
+  match e with
+  | Z0 => zq
+  | Zpos e => IRmult zq (IRZ (IZpow_pos 10 e))
+  | Zneg e => IRdiv zq (IRZ (IZpow_pos 10 e))
+  end.
+
+Definition of_hexadecimal (d : Hexadecimal.hexadecimal) : IR :=
+  let '(i, f, e) :=
+    match d with
+    | Hexadecimal.Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil)
+    | Hexadecimal.HexadecimalExp i f e => (i, f, e)
+    end in
+  let zq := match f with
+    | Hexadecimal.Nil => IRZ (IZ_of_Z (Z.of_hex_int i))
+    | _ =>
+      let num := Z.of_hex_int (Hexadecimal.app_int i f) in
+      let den := Nat.iter (Hexadecimal.nb_digits f) (Pos.mul 16) 1%positive in
+      IRQ (Qmake num den) end in
+  let e := Z.of_int e in
+  match e with
+  | Z0 => zq
+  | Zpos e => IRmult zq (IRZ (IZpow_pos 2 e))
+  | Zneg e => IRdiv zq (IRZ (IZpow_pos 2 e))
+  end.
+
+Definition of_number (n : Number.number) : IR :=
+  match n with
+  | Number.Dec d => of_decimal d
+  | Number.Hex h => of_hexadecimal h
+  end.
+
+Definition to_decimal (n : IR) : option Decimal.decimal :=
+  match n with
+  | IRZ z =>
+    match IZ_to_Z z with
+    | Some z => Some (Decimal.Decimal (Z.to_int z) Decimal.Nil)
+    | None => None
+    end
+  | IRQ (Qmake num den) => IQmake_to_decimal num den
+  | IRmult (IRZ z) (IRZ (IZpow_pos 10 e)) =>
+    match IZ_to_Z z with
+    | Some z =>
+      Some (Decimal.DecimalExp (Z.to_int z) Decimal.Nil (Pos.to_int e))
+    | None => None
+    end
+  | IRmult (IRQ (Qmake num den)) (IRZ (IZpow_pos 10 e)) =>
+    match IQmake_to_decimal num den with
+    | Some (Decimal.Decimal i f) =>
+      Some (Decimal.DecimalExp i f (Pos.to_int e))
+    | _ => None
+    end
+  | IRdiv (IRZ z) (IRZ (IZpow_pos 10 e)) =>
+    match IZ_to_Z z with
+    | Some z =>
+      Some (Decimal.DecimalExp (Z.to_int z) Decimal.Nil (Decimal.Neg (Pos.to_uint e)))
+    | None => None
+    end
+  | IRdiv (IRQ (Qmake num den)) (IRZ (IZpow_pos 10 e)) =>
+    match IQmake_to_decimal num den with
+    | Some (Decimal.Decimal i f) =>
+      Some (Decimal.DecimalExp i f (Decimal.Neg (Pos.to_uint e)))
+    | _ => None
+    end
+  | _ => None
+  end.
+
+Definition to_hexadecimal (n : IR) : option Hexadecimal.hexadecimal :=
+  match n with
+  | IRZ z =>
+    match IZ_to_Z z with
+    | Some z => Some (Hexadecimal.Hexadecimal (Z.to_hex_int z) Hexadecimal.Nil)
+    | None => None
+    end
+  | IRQ (Qmake num den) => IQmake_to_hexadecimal num den
+  | IRmult (IRZ z) (IRZ (IZpow_pos 2 e)) =>
+    match IZ_to_Z z with
+    | Some z =>
+      Some (Hexadecimal.HexadecimalExp (Z.to_hex_int z) Hexadecimal.Nil (Pos.to_int e))
+    | None => None
+    end
+  | IRmult (IRQ (Qmake num den)) (IRZ (IZpow_pos 2 e)) =>
+    match IQmake_to_hexadecimal num den with
+    | Some (Hexadecimal.Hexadecimal i f) =>
+      Some (Hexadecimal.HexadecimalExp i f (Pos.to_int e))
+    | _ => None
+    end
+  | IRdiv (IRZ z) (IRZ (IZpow_pos 2 e)) =>
+    match IZ_to_Z z with
+    | Some z =>
+      Some (Hexadecimal.HexadecimalExp (Z.to_hex_int z) Hexadecimal.Nil (Decimal.Neg (Pos.to_uint e)))
+    | None => None
+    end
+  | IRdiv (IRQ (Qmake num den)) (IRZ (IZpow_pos 2 e)) =>
+    match IQmake_to_hexadecimal num den with
+    | Some (Hexadecimal.Hexadecimal i f) =>
+      Some (Hexadecimal.HexadecimalExp i f (Decimal.Neg (Pos.to_uint e)))
+    | _ => None
+    end
+  | _ => None
+  end.
+
+Definition to_number q :=
+  match to_decimal q with
+  | None => None
+  | Some q => Some (Number.Dec q)
+  end.
+
+Definition to_hex_number q :=
+  match to_hexadecimal q with
+  | None => None
+  | Some q => Some (Number.Hex q)
+  end.
+
+Number Notation R of_number to_hex_number (via IR
+  mapping [IZR => IRZ, Q2R => IRQ, Rmult => IRmult, Rdiv => IRdiv,
+           Z.pow_pos => IZpow_pos, Z0 => IZ0, Zpos => IZpos, Zneg => IZneg])
+  : hex_R_scope.
+
+Number Notation R of_number to_number (via IR
+  mapping [IZR => IRZ, Q2R => IRQ, Rmult => IRmult, Rdiv => IRdiv,
+           Z.pow_pos => IZpow_pos, Z0 => IZ0, Zpos => IZpos, Zneg => IZneg])
+  : R_scope.
diff --git a/theories/Reals/Rregisternames.v b/theories/Reals/Rregisternames.v
index 8b078f2cf3..8117d975fe 100644
--- a/theories/Reals/Rregisternames.v
+++ b/theories/Reals/Rregisternames.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Raxioms Rfunctions Qreals.
+Require Import Raxioms Rfunctions.
 
 (*****************************************************************)
 (**           Register names for use in plugins                  *)
@@ -31,4 +31,4 @@ Register IZR as reals.R.IZR.
 Register Rabs as reals.R.Rabs.
 Register powerRZ as reals.R.powerRZ.
 Register pow as reals.R.pow.
-Register Qreals.Q2R as reals.R.Q2R.
+Register Q2R as reals.R.Q2R.
diff --git a/theories/dune b/theories/dune
index c2d8197ee4..e7e4ba9981 100644
--- a/theories/dune
+++ b/theories/dune
@@ -17,7 +17,6 @@
    coq.plugins.numeral_notation
    coq.plugins.string_notation
    coq.plugins.int63_syntax
-   coq.plugins.r_syntax
    coq.plugins.float_syntax
 
    coq.plugins.btauto