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/patternops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 99c3772db9..aa795106a8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -204,7 +204,7 @@ let error_instantiate_pattern id l =
   | [_] -> "is" 
   | _ -> "are"
   in
-  errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+  user_err "" (str "Cannot substitute the term bound to " ++ pr_id id
     ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
-- 
cgit v1.2.3