From 08189431706298d599cffea2e41dd51290305ba3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jan 2020 13:36:34 +0100
Subject: Centralizing all kinds of numeral string management in numTok.ml.

Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent

In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.

Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
---
 printing/ppconstr.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 21b9cd4f1f..b285c0abcc 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -77,8 +77,8 @@ let tag_var = tag Tag.variable
     | LevelSome -> true
 
   let prec_of_prim_token = function
-    | Numeral (SPlus,_) -> lposint
-    | Numeral (SMinus,_) -> lnegint
+    | Numeral (NumTok.SPlus,_) -> lposint
+    | Numeral (NumTok.SMinus,_) -> lnegint
     | String _ -> latom
 
   let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
@@ -222,8 +222,7 @@ let tag_var = tag Tag.variable
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t
 
   let pr_prim_token = function
-    | Numeral (SPlus,n) -> str (NumTok.to_string n)
-    | Numeral (SMinus,n) -> str ("-"^NumTok.to_string n)
+    | Numeral n -> NumTok.Signed.print n
     | String s -> qs s
 
   let pr_evar pr id l =
-- 
cgit v1.2.3