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 /lib/pp.ml4 | |
| 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 'lib/pp.ml4')
| -rw-r--r-- | lib/pp.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 0a3466859e..35621a5d7c 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -327,6 +327,7 @@ let flush_all() = flush stderr; flush stdout; pp_flush() (* pretty printing functions WITH FLUSH *) let msg x = msg_with !std_ft x let msgnl x = msgnl_with !std_ft x +let msg_info x = msgnl x let msgerr x = msg_with !err_ft x let msgerrnl x = msgnl_with !err_ft x let msg_warning x = msg_warning_with !err_ft x |