From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 21 Feb 2008 18:57:28 +0000 (+0000)
Subject: Avoid application to 0 arguments.
X-Git-Tag: make_still_working~5584
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec180828486193a293203ce7f24632b0290b7fca;p=helm.git

Avoid application to 0 arguments.
---

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 *)