From ec180828486193a293203ce7f24632b0290b7fca Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 21 Feb 2008 18:57:28 +0000 Subject: [PATCH] Avoid application to 0 arguments. --- .../components/ng_kernel/oCic2NCic.ml | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 0d00f031f..1d0e453b0 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -46,17 +46,19 @@ let splat_args_for_rel ctx t = let splat_args ctx t n_fix = let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in - let rec aux = function - | 0 -> [] - | n -> - (match List.nth ctx (n-1) with - | Ce _ when n <= bound -> NCic.Rel n - | Fix (refe, _, _) when n < primo_ce_dopo_fix -> - splat_args_for_rel ctx (NCic.Const refe) - | Fix _ | Ce _ -> NCic.Rel (n - n_fix) - ) :: aux (n-1) - in - NCic.Appl (t:: aux (List.length ctx)) + if ctx = [] then t + else + let rec aux = function + | 0 -> [] + | n -> + (match List.nth ctx (n-1) with + | Ce _ when n <= bound -> NCic.Rel n + | Fix (refe, _, _) when n < primo_ce_dopo_fix -> + splat_args_for_rel ctx (NCic.Const refe) + | Fix _ | Ce _ -> NCic.Rel (n - n_fix) + ) :: aux (n-1) + in + NCic.Appl (t:: aux (List.length ctx)) ;; (* we are lambda-lifting also variables that do not occur *) -- 2.39.2