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.
---
 engine/logic_monad.ml | 2 +-
 engine/proofview.ml   | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 17ff898b0f..e14a2bd396 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -34,7 +34,7 @@ exception Timeout
 exception TacticFailure of exn
 
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
+  | Timeout -> CErrors.user_err "Some timeout function" (Pp.str"Timeout!")
   | Exception e -> CErrors.print e
   | TacticFailure e -> CErrors.print e
   | _ -> Pervasives.raise CErrors.Unhandled
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 576569cf5f..c47c44e222 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -365,7 +365,7 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
     let suffix = !nosuchgoals_hook n in
-    CErrors.errorlabstrm ""
+    CErrors.user_err ""
       (str "No such " ++ str (String.plural n "goal") ++ str "." ++
        pr_non_empty_arg (fun x -> x) suffix)
       | _ -> raise CErrors.Unhandled
@@ -451,7 +451,7 @@ let _ = CErrors.register_handler begin function
         str"Incorrect number of goals" ++ spc() ++
         str"(expected "++int i++str(String.plural i " tactic") ++ str")."
       in
-      CErrors.errorlabstrm "" errmsg
+      CErrors.user_err "" errmsg
   | _ -> raise CErrors.Unhandled
 end
 
@@ -849,7 +849,7 @@ let tclPROGRESS t =
 
 exception Timeout
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Timeout -> CErrors.user_err "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> Pervasives.raise CErrors.Unhandled
 end
 
-- 
cgit v1.2.3