From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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.
---
 proofs/pfedit.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/pfedit.ml')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e4bae2012..b86582def 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -131,7 +131,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     | CList.IndexOutOfRange ->
         match gi with
 	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
-	                            CErrors.errorlabstrm "" msg
+	                            CErrors.user_err "" msg
         | _ -> assert false
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
-- 
cgit v1.2.3