aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:15 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-12 20:49:15 +0000
commit1638f5df49ff81e174f6a1c6915a65c9b9d4adf5 (patch)
treeb3156dbc48bed485132a0e9cbca59a1c82bc1d9a /toplevel
parentcf6b384b17a66686f31001d8aeb0958f3cfbfbea (diff)
Remove print call that do not use the pp mechanism
Signed-off-by: Edward Z. Yang <ezyang@mit.edu> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index fe6e350e6..cb14ff482 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -29,7 +29,7 @@ let get_version_date () =
let print_header () =
let (ver,rev) = (get_version_date ()) in
- Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
+ pp (str "Welcome to Coq "++ str ver ++ str " (" ++ str rev ++ str ")\n");
flush stdout
let output_context = ref false
@@ -38,7 +38,7 @@ let memory_stat = ref false
let print_memory_stat () =
if !memory_stat then
- Format.printf "total heap size = %d kbytes\n" (heap_size_kb ())
+ pp (str "total heap size = " ++ int (heap_size_kb ()) ++ str " kbytes" ++ fnl ())
let _ = at_exit print_memory_stat