diff options
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 134b6ba94..a78532e33 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -74,7 +74,7 @@ END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY | [ "Print" "Firstorder" "Solver" ] -> [ - Pp.msg_info + Feedback.msg_info (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] END @@ -131,7 +131,7 @@ ARGUMENT EXTEND firstorder_using | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] | [ "using" reference(a) reference(b) reference_list(l) ] -> [ Flags.if_verbose - Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); + Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); a::b::l ] | [ ] -> [ [] ] |