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. --- pretyping/find_subterm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/find_subterm.ml') diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 4caa1e992..c7909a3c7 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -35,7 +35,7 @@ let explain_occurrence_error = function | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id let error_occurrences_error e = - errorlabstrm "" (explain_occurrence_error e) + user_err "" (explain_occurrence_error e) let error_invalid_occurrence occ = error_occurrences_error (InvalidOccurrence occ) -- cgit v1.2.3