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
---
 plugins/funind/indfun.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/funind/indfun.ml')

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)
-- 
cgit v1.2.3