From 7d33d9c1837149d31df06b803ed4dbf2ce4053ca Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 9 Jan 2019 11:02:13 +0000
Subject: Coq: add parens around negative integer literals

---
 src/pretty_print_coq.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 08844eb5..5cf17056 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -585,8 +585,9 @@ let doc_lit (L_aux(lit,l)) =
   | L_false -> utf8string "false"
   | L_true  -> utf8string "true"
   | L_num i ->
-     let ipp = Big_int.to_string i in
-     utf8string ipp
+     let s = Big_int.to_string i in
+     let ipp = utf8string s in
+     if Big_int.less i Big_int.zero then parens ipp else ipp
   | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_undef ->
-- 
cgit v1.2.3