diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 11f45d5d8..0d4be72d9 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -19,7 +19,8 @@ open Names open Pp open Pcoq open Genarg -open Constrarg +open Stdarg +open Tacarg open Term open Vars open Topconstr @@ -41,7 +42,7 @@ open Proofview.Notations open Tacinterp open Pretyping open Constr -open Tactic +open Pltac open Extraargs open Ppconstr open Printer @@ -61,8 +62,8 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = CErrors.errorlabstrm "ssrmatching" -let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) +let errorstrm = CErrors.user_err ~hdr:"ssrmatching" +let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) |