From 94c8f42eea1c36f582fe2390680de75634324c85 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 1 Aug 2019 15:14:42 +0200
Subject: [cleanup] Replace uses of UserError constructor, clarify exception
 names.

We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.

We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.

cc: #7560
---
 engine/logic_monad.ml  | 5 ++---
 engine/logic_monad.mli | 2 +-
 engine/proofview.ml    | 8 ++++----
 engine/proofview.mli   | 2 --
 4 files changed, 7 insertions(+), 10 deletions(-)

(limited to 'engine')

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 7c06bb59f1..e3a5676942 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -30,7 +30,7 @@
 exception Exception of exn
 
 (** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
 
 (** This exception is used by the tactics to signal failure by lack of
     successes, rather than some other exceptions (like system
@@ -38,7 +38,6 @@ exception Timeout
 exception TacticFailure of exn
 
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!")
   | Exception e -> CErrors.print e
   | TacticFailure e -> CErrors.print e
   | _ -> raise CErrors.Unhandled
@@ -99,7 +98,7 @@ struct
   let print_char = fun c -> (); fun () -> print_char c
 
   let timeout = fun n t -> (); fun () ->
-    Control.timeout n t () (Exception Timeout)
+    Control.timeout n t () (Exception Tac_Timeout)
 
   let make f = (); fun () ->
     try f ()
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 90c920439a..75920455ce 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -30,7 +30,7 @@
 exception Exception of exn
 
 (** This exception is used to signal abortion in [timeout] functions. *)
-exception Timeout
+exception Tac_Timeout
 
 (** This exception is used by the tactics to signal failure by lack of
     successes, rather than some other exceptions (like system
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8b5bd4cd80..8b8382ea53 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -905,11 +905,10 @@ let tclPROGRESS t =
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError (Some "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 ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -934,7 +933,8 @@ let tclTIMEOUT n t =
       end
       begin let open Logic_monad.NonLogical in function (e, info) ->
         match e with
-        | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
+        | Logic_monad.Tac_Timeout ->
+          return (Util.Inr (Logic_monad.Tac_Timeout, info))
         | Logic_monad.TacticFailure e ->
           return (Util.Inr (e, info))
         | e -> Logic_monad.NonLogical.raise ~info e
diff --git a/engine/proofview.mli b/engine/proofview.mli
index f90f02f3e1..a17a1c9951 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -404,8 +404,6 @@ end
 (** Checks for interrupts *)
 val tclCHECKINTERRUPT : unit tactic
 
-exception Timeout
-
 (** [tclTIMEOUT n t] can have only one success.
     In case of timeout if fails with [tclZERO Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
-- 
cgit v1.2.3