diff options
| -rw-r--r-- | parsing/lexer.ml4 | 2 | ||||
| -rw-r--r-- | parsing/tok.ml | 2 | ||||
| -rw-r--r-- | parsing/tok.mli | 1 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 6 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 |
5 files changed, 5 insertions, 10 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index e351061dcd..46dd516be8 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -94,8 +94,6 @@ module Error = struct | UnsupportedUnicode x -> Printf.sprintf "Unsupported Unicode character (0x%x)" x) - let print ppf x = Format.fprintf ppf "%s@." (to_string x) - end open Error diff --git a/parsing/tok.ml b/parsing/tok.ml index bd7645c2ba..69fcca98d7 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -45,8 +45,6 @@ let match_keyword kwd = function | KEYWORD kwd' when kwd = kwd' -> true | _ -> false -let print ppf tok = Format.fprintf ppf "%s" (to_string tok) - (** For camlp5, conversion from/to [Plexing.pattern], and a match function analoguous to [Plexing.default_match] *) diff --git a/parsing/tok.mli b/parsing/tok.mli index 9a1edec578..d3c178b5a3 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -21,7 +21,6 @@ type t = val extract_string : t -> string val to_string : t -> string -val print : Format.formatter -> t -> unit val match_keyword : string -> t -> bool (** for camlp5 *) val of_pattern : string*string -> t diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index a0187434aa..fb9439d73e 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -139,11 +139,11 @@ and e_my_find_search db_list local_db hdc concl = in (tac,lazy (pr_autotactic t))) (*i - fun gls -> pPNL (pr_autotactic t); Format.print_flush (); + fun gls -> pPNL (pr_autotactic t); pp_flush (); try tac gls with e when Logic.catchable_exception(e) -> - (Format.print_string "Fail\n"; - Format.print_flush (); + (str "Fail\n"; + pp_flush (); raise e) i*) in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index fe6e350e6e..cb14ff4820 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 |