diff options
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.ml4')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 536c6ff4b..199c26363 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -61,7 +61,7 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = CErrors.errorlabstrm "ssrmatching" +let errorstrm = CErrors.user_err "ssrmatching" let loc_error loc msg = CErrors.user_err ~loc msg (str msg) let ppnl = Feedback.msg_info |