Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify exception names

Reviewed-by: ppedrot

11 files changed, 46 insertions, 19 deletions

diff --git a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh
new file mode 100644
index 0000000000..21ff60493b
--- /dev/null
+++ b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then
+
+    coqhammer_CI_REF=errors+private
+    coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
+
+fi
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
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index ddd6ecfb5c..7c17ecdba0 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1252,7 +1252,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
-      raise (UserError(Some "compute_cst_params", str "Not handled case"))
+    CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case")
   ) gt
 and compute_cst_params_from_app acc (params,rtl) =
   let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index fbf63c69dd..8abccabae6 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,4 +1,13 @@
-open Pp
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open Constr
 open Glob_term
 open CErrors
@@ -433,7 +442,8 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
 	     )
-      | GRec _ -> raise (UserError(None,str "Not handled GRec"))
+      | GRec _ ->
+        CErrors.user_err (Pp.str "Not handled GRec")
       | GSort _
       | GHole _ as rt -> rt
       | GInt _ as rt -> rt
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 24b3690138..70211a1860 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open Names
 open Glob_term
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2937ae5d14..a205c0744a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -95,7 +95,8 @@ let functional_induction with_clean c princl pat =
           (* We need to refresh gl due to the updated evar_map in princ *)
           Proofview.Goal.enter_one (fun gl ->
           Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args))
-        | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
+        | _ ->
+          CErrors.user_err (str "functional induction must be used with a function" )
       end
     | Some ((princ,binding)) ->
       Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7719705138..16c0521eda 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -40,7 +40,9 @@ let locate_constant ref =
 
 let locate_with_msg msg f x =
   try f x
-  with Not_found -> raise (CErrors.UserError(None, msg))
+  with
+  | Not_found ->
+    CErrors.user_err msg
 
 
 let filter_map filter f =
@@ -64,8 +66,7 @@ let chop_rlambda_n  =
           | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
           | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
           | _ ->
-              raise (CErrors.UserError(Some "chop_rlambda_n",
-                                    str "chop_rlambda_n: Not enough Lambdas"))
+            CErrors.user_err ~hdr:"chop_rlambda_n" (str "chop_rlambda_n: Not enough Lambdas")
   in
   chop_lambda_n []
 
@@ -76,7 +77,8 @@ let chop_rprod_n  =
       else
         match DAst.get rt with
           | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
-          | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
+          | _ ->
+            CErrors.user_err ~hdr:"chop_rprod_n" (str "chop_rprod_n: Not enough products")
   in
   chop_prod_n []
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2d0806b2e0..b93c4a176f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -546,7 +546,8 @@ module New = struct
     Proofview.tclOR
       (Proofview.tclTIMEOUT n t)
       begin function (e, info) -> match e with
-        | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
+        | Logic_monad.Tac_Timeout as e ->
+          Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
         | e -> Proofview.tclZERO ~info e
       end