diff options
| author | Pierre-Marie Pédrot | 2019-08-29 14:39:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-29 14:39:59 +0200 |
| commit | 60b9352656b95b7e5c46c9f28fec3a171f3fc74a (patch) | |
| tree | fec69b141cf2e71dd9789567b001ca3df55c776b /plugins/funind/glob_termops.ml | |
| parent | 737955a82676cab8de7283bf23db3962dd6a3792 (diff) | |
| parent | 94c8f42eea1c36f582fe2390680de75634324c85 (diff) | |
Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify exception names
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 14 |
1 files changed, 12 insertions, 2 deletions
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 |