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/cc/cctac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/cc/cctac.ml') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index fd46d8069..6ed678176 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -456,7 +456,7 @@ let cc_tactic depth additionnal_terms = end } let cc_fail gls = - errorlabstrm "Congruence" (Pp.str "congruence failed.") + user_err "Congruence" (Pp.str "congruence failed.") let congruence_tac depth l = Tacticals.New.tclORELSE -- cgit v1.2.3