aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/glob_termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/glob_termops.ml')
-rw-r--r--plugins/funind/glob_termops.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0159a0aeeb..6b4fbeef46 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -531,8 +531,8 @@ let rec are_unifiable_aux = function
then raise NotUnifiable
else
let eqs' =
- try ((List.combine cpl1 cpl2)@eqs)
- with _ -> anomaly (Pp.str "are_unifiable_aux")
+ try (List.combine cpl1 cpl2) @ eqs
+ with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux")
in
are_unifiable_aux eqs'
@@ -553,8 +553,8 @@ let rec eq_cases_pattern_aux = function
then raise NotUnifiable
else
let eqs' =
- try ((List.combine cpl1 cpl2)@eqs)
- with _ -> anomaly (Pp.str "eq_cases_pattern_aux")
+ try (List.combine cpl1 cpl2) @ eqs
+ with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux")
in
eq_cases_pattern_aux eqs'
| _ -> raise NotUnifiable