aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto')
-rw-r--r--plugins/rtauto/refl_tauto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index ceaf2a79b..597b6afb6 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -122,7 +122,7 @@ let rec make_form atom_env gls term =
let fb=make_form atom_env gls argv.(1) in
Disjunct (fa,fb)
else make_atom atom_env (normalize term)
- with Invalid_argument _ -> make_atom atom_env (normalize term)
+ with DestKO -> make_atom atom_env (normalize term)
end
| _ -> make_atom atom_env (normalize term)