X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=1d0e453b006457909f1bb6a5c55fe33c27c4667e;hb=8da8820a77f2104dd1bf17c01fa77f75ee31c8fb;hp=0d00f031f18c558cbba117337fe7bda33ca8c440;hpb=bd5488c8eaa88e27d6e9e6c46566f1ed8f1a59b0;p=helm.git

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