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

(limited to 'engine/proofview.ml')

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


From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 02:35:47 +0200
Subject: Make the user_err header an optional parameter.

Suggested by @ppedrot
---
 engine/proofview.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'engine/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index c47c44e222..51b3a7260a 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.user_err ""
+    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.user_err "" errmsg
+      CErrors.user_err  errmsg
   | _ -> raise CErrors.Unhandled
 end
 
@@ -845,11 +845,11 @@ let tclPROGRESS t =
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
+    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
 
 exception Timeout
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.user_err "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> Pervasives.raise CErrors.Unhandled
 end
 
-- 
cgit v1.2.3