diff options
| author | ppedrot | 2012-05-30 16:51:34 +0000 |
|---|---|---|
| committer | ppedrot | 2012-05-30 16:51:34 +0000 |
| commit | 4d58a4f25a796d1c5d39f2be8648696cdfd46dba (patch) | |
| tree | 3b2587eb464393caf23a50283c10f80532ace22f /proofs | |
| parent | 24879dc0e59856e297b0172d00d67df67fbb0184 (diff) | |
Getting rid of Pp.msg
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 221c46a926..cb588af2d3 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -89,7 +89,7 @@ let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - msg (hov 0 s); tclIDTAC gls + pp (hov 0 s); pp_flush (); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) 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 |