diff options
| author | Pierre-Marie Pédrot | 2016-09-08 14:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 15:41:16 +0200 |
| commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
| tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /plugins/ssrmatching | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index ff1db8cf53..5fb0bb6647 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -61,8 +61,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 *) |