From 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 19 Oct 2018 13:16:25 +0200
Subject: Replace type sign = bool with SPlus | SMinus

---
 printing/ppconstr.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 229930142e..1c496efb8f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -84,7 +84,8 @@ let tag_var = tag Tag.variable
         | Any -> true
 
   let prec_of_prim_token = function
-    | Numeral (_,b) -> if b then lposint else lnegint
+    | Numeral (SPlus,_) -> lposint
+    | Numeral (SMinus,_) -> lnegint
     | String _ -> latom
 
   let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
@@ -234,7 +235,8 @@ let tag_var = tag Tag.variable
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
   let pr_prim_token = function
-    | Numeral (n,s) -> str (if s then n else "-"^n)
+    | Numeral (SPlus,n) -> str n
+    | Numeral (SMinus,n) -> str ("-"^n)
     | String s -> qs s
 
   let pr_evar pr id l =
-- 
cgit v1.2.3


From 552bb5aba750785d8f19aa7b333baa59e9199369 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 14:40:23 +0200
Subject: Add parsing of decimal constants (e.g., 1.02e+01)

Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.

This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`

See examples of each use case in the next two commits.
---
 printing/ppconstr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1c496efb8f..0ae3de7321 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -235,8 +235,8 @@ let tag_var = tag Tag.variable
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
   let pr_prim_token = function
-    | Numeral (SPlus,n) -> str n
-    | Numeral (SMinus,n) -> str ("-"^n)
+    | Numeral (SPlus,n) -> str (NumTok.to_string n)
+    | Numeral (SMinus,n) -> str ("-"^NumTok.to_string n)
     | String s -> qs s
 
   let pr_evar pr id l =
-- 
cgit v1.2.3