aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/indfun_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun_common.ml')
-rw-r--r--plugins/funind/indfun_common.ml9
1 files changed, 3 insertions, 6 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c6f5c2745..848b44a60 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -21,12 +21,9 @@ let get_name avoid ?(default="H") = function
| Name n -> Name n
let array_get_start a =
- try
- Array.init
- (Array.length a - 1)
- (fun i -> a.(i))
- with Invalid_argument "index out of bounds" ->
- invalid_arg "array_get_start"
+ Array.init
+ (Array.length a - 1)
+ (fun i -> a.(i))
let id_of_name = function
Name id -> id