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

Reviewed-by: ppedrot

5 files changed, 31 insertions, 8 deletions

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 []