From 4d58a4f25a796d1c5d39f2be8648696cdfd46dba Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 30 May 2012 16:51:34 +0000 Subject: Getting rid of Pp.msg git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/tactic_debug.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs/tactic_debug.ml') diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index b23f361c7c..d09c7f05ad 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -60,7 +60,7 @@ let help () = let goal_com g tac = begin db_pr_goal g; - msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ()) + msgnl (str "Going to execute:" ++ fnl () ++ !prtac tac) end let skipped = ref 0 @@ -105,14 +105,14 @@ let run ini = for i=1 to 2 do print_char (Char.chr 8);print_char (Char.chr 13) done; - msg (str "Executed expressions: " ++ int !skipped ++ fnl() ++ fnl()) + msgnl (str "Executed expressions: " ++ int !skipped ++ fnl()) end; incr skipped (* Prints the prompt *) let rec prompt level = begin - msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > "); + pp (fnl () ++ str "TcDebug (" ++ int level ++ str ") > "); flush stdout; let exit () = skip:=0;skipped:=0;raise Sys.Break in let inst = try read_line () with End_of_file -> exit () in -- cgit v1.2.3