diff options
Diffstat (limited to 'lib/pp_control.ml')
| -rw-r--r-- | lib/pp_control.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 3b1266c2c..44f351458 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -22,7 +22,7 @@ let dflt_gp = { margin = 72; max_indent = 62; max_depth = 50; - ellipsis = "." } + ellipsis = ".." } (* A deeper pretty-printer to print proof scripts *) @@ -30,7 +30,7 @@ let deep_gp = { margin = 72; max_indent = 62; max_depth = 10000; - ellipsis = "." } + ellipsis = "..." } (* set_gp : Format.formatter -> pp_global_params -> unit * set the parameters of a formatter *) |