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/glob_termops.ml | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

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

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