A new very simple example for recursive functions. Still bugged, but getting

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0d00f031f18c558cbba117337fe7bda33ca8c440..1d0e453b006457909f1bb6a5c55fe33c27c4667e 100644 (file)
--- 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 *)