X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=c1b450e612d627135a6f982dbbb2088d8c12b1cb;hb=46219a352fd586e1f89237effdcb037a6e371969;hp=245308d12235e346599b1940e9e16ed48b8aa900;hpb=9cfd71df3f877fac9556993da6a88b51ba05fdc6;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 245308d12..c1b450e61 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -121,7 +121,10 @@ let splat_args_for_rel ctx t ?rels n_fix =
           | `Ce ((_, NCic.Def _),_) -> aux (n-1,tl))
       | _,_ -> assert false
     in
-    NCic.Appl (t:: aux (List.length ctx,rels))
+   let args = aux (List.length ctx,rels) in
+    match args with
+       [] -> t
+     | _::_ -> NCic.Appl (t::args)
 ;;
 
 let splat_args ctx t n_fix rels =