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.
---
 printing/prettyp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index a7742d866e..e2fefa5c8f 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -736,7 +736,7 @@ let print_any_name = function
     let open Context.Named.Declaration in
     str |> Global.lookup_named |> set_id str |> print_named_decl
   with Not_found ->
-    errorlabstrm
+    user_err
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
 let print_name = function
@@ -831,7 +831,7 @@ let index_of_class cl =
   try
     fst (class_info cl)
   with Not_found ->
-    errorlabstrm "index_of_class"
+    user_err "index_of_class"
       (pr_class cl ++ spc() ++ str "not a defined class.")
 
 let print_path_between cls clt =
@@ -841,7 +841,7 @@ let print_path_between cls clt =
     try
       lookup_path_between_class (i,j)
     with Not_found ->
-      errorlabstrm "index_cl_of_id"
+      user_err "index_cl_of_id"
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
 	 ++ str ".")
   in
-- 
cgit v1.2.3