aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-15 22:00:17 +0200
committerMaxime Dénès2017-06-15 22:00:17 +0200
commit6467119bd15395bb5fae7d9c19dde17293842bd8 (patch)
tree809a7156570542f796b4ed94d901a83468d78dc4 /printing
parent9beec0fc6cc283294bbbda363a3f788ae56347d5 (diff)
parent0b5ef21f936acbb89fa5b272efdcf3cf03de58cc (diff)
Merge PR#719: Constrexpr.Numeral without bigint
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 626464b96f..49eedb767b 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -80,7 +80,7 @@ let tag_var = tag Tag.variable
| Any -> true
let prec_of_prim_token = function
- | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
+ | Numeral (_,b) -> if b then lposint else lnegint
| String _ -> latom
open Notation
@@ -231,7 +231,7 @@ let tag_var = tag Tag.variable
| ArgVar (loc,s) -> pr_lident (loc,s)
let pr_prim_token = function
- | Numeral n -> str (Bigint.to_string n)
+ | Numeral (n,s) -> str (if s then n else "-"^n)
| String s -> qs s
let pr_evar pr id l =