From b6c13afd432ce1957315e94c1ce8c06aa848fe5a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:19:00 +0200
Subject: [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.
---
 plugins/syntax/dune | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'plugins/syntax/dune')

diff --git a/plugins/syntax/dune b/plugins/syntax/dune
index b395695c8a..1b3d7598da 100644
--- a/plugins/syntax/dune
+++ b/plugins/syntax/dune
@@ -12,13 +12,6 @@
  (modules g_string string_notation)
  (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)
-- 
cgit v1.2.3


From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 plugins/syntax/dune | 17 +++++------------
 1 file changed, 5 insertions(+), 12 deletions(-)

(limited to 'plugins/syntax/dune')

diff --git a/plugins/syntax/dune b/plugins/syntax/dune
index 1b3d7598da..f930fc265a 100644
--- a/plugins/syntax/dune
+++ b/plugins/syntax/dune
@@ -1,15 +1,8 @@
 (library
- (name numeral_notation_plugin)
- (public_name coq.plugins.numeral_notation)
- (synopsis "Coq numeral notation plugin")
- (modules g_numeral numeral)
- (libraries coq.vernac))
-
-(library
- (name string_notation_plugin)
- (public_name coq.plugins.string_notation)
- (synopsis "Coq string notation plugin")
- (modules g_string string_notation)
+ (name number_string_notation_plugin)
+ (public_name coq.plugins.number_string_notation)
+ (synopsis "Coq number and string notation plugin")
+ (modules g_number_string string_notation number)
  (libraries coq.vernac))
 
 (library
@@ -26,4 +19,4 @@
  (modules float_syntax)
  (libraries coq.vernac))
 
-(coq.pp (modules g_numeral g_string))
+(coq.pp (modules g_number_string))
-- 
cgit v1.2.3