From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 01:58:04 +0200 Subject: Remove errorlabstrm in favor of user_err As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch. --- plugins/ssrmatching/ssrmatching.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssrmatching') 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 -- cgit v1.2.3