aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/cic2acic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index a0faa6426e..54510ba179 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -697,7 +697,7 @@ print_endline "PASSATO" ; flush stdout ;
let
compute_result_if_eta_expansion_not_required subst residual_args
=
- let residual_args_not_empty = List.length residual_args > 0 in
+ let residual_args_not_empty = residual_args <> [] in
let h' =
if residual_args_not_empty then
aux' env idrefs ~subst:(None,subst) h