diff options
| author | ppedrot | 2012-06-01 18:03:06 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 18:03:06 +0000 |
| commit | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (patch) | |
| tree | 5f3fd167f5dd704bf5482d236624aa8ef8bf6707 /parsing | |
| parent | 35e4ac349af4fabbc5658b5cba632f98ec04da3f (diff) | |
Getting rid of Pp.msgnl and Pp.message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_obligations.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index d4229ff0b0..7d7f2b10d3 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -126,7 +126,7 @@ open Pp VERNAC COMMAND EXTEND Show_Solver | [ "Show" "Obligation" "Tactic" ] -> [ - msgnl (str"Program obligation tactic is " ++ print_default_tactic ()) ] + msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] END VERNAC COMMAND EXTEND Show_Obligations @@ -135,8 +135,8 @@ VERNAC COMMAND EXTEND Show_Obligations END VERNAC COMMAND EXTEND Show_Preterm -| [ "Preterm" "of" ident(name) ] -> [ show_term (Some name) ] -| [ "Preterm" ] -> [ show_term None ] +| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] +| [ "Preterm" ] -> [ msg_info (show_term None) ] END open Pp |