summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2014-04-08 14:15:38 +0100
committerKathy Gray2014-04-08 14:15:38 +0100
commitfa3c145f68d9865ee48abe171f5958a1f154cd0a (patch)
tree61bb990f864a8374966496b0ea5b90506ac7adef /src
parent7087e8973bc4ecbe6366ea23425ff46d3ebe2041 (diff)
Try to reduce size of Lem output a little bit
Diffstat (limited to 'src')
-rw-r--r--src/pretty_print.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 4ce89f71..153147d3 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -584,7 +584,7 @@ let pp_format_tag = function
let pp_format_nes nes =
"[" ^
- (list_format "; "
+ (*(list_format "; "
(fun ne -> match ne with
| LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
| Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
@@ -594,7 +594,7 @@ let pp_format_nes nes =
| InS(_,{nexp = Nuvar _},ns) | InOpen(_,{nexp = Nuvar _},ns) ->
"(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"
)
- nes) ^ "]"
+ nes) ^*) "]"
let pp_format_annot = function
| None -> "Nothing"