diff options
Diffstat (limited to 'ltac/g_obligations.ml4')
| -rw-r--r-- | ltac/g_obligations.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4 index 4cd8bf1fe..987b9d538 100644 --- a/ltac/g_obligations.ml4 +++ b/ltac/g_obligations.ml4 @@ -121,7 +121,7 @@ open Pp VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY | [ "Show" "Obligation" "Tactic" ] -> [ - msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] + Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] END VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY @@ -130,8 +130,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] -| [ "Preterm" ] -> [ msg_info (show_term None) ] +| [ "Preterm" "of" ident(name) ] -> [ Feedback.msg_info (show_term (Some name)) ] +| [ "Preterm" ] -> [ Feedback.msg_info (show_term None) ] END open Pp |