diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 67f6fdd543..d6a017d08c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -49,11 +49,8 @@ let locate_constant ref = let locate_with_msg msg f x = - try - f x - with - | Not_found -> raise (Errors.UserError("", msg)) - | e -> raise e + try f x + with Not_found -> raise (Errors.UserError("", msg)) let filter_map filter f = |