From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 1 May 2008 14:11:07 +0000 (+0000)
Subject: Last (???) bug about variables with bodies fixed: we do no longer create
X-Git-Tag: make_still_working~5263
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7bb53e63c15cf501c98881839a2fdc19a6c88028;p=helm.git

Last (???) bug about variables with bodies fixed: we do no longer create
applications with less than 2 args.
---

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index 45867405f..7abd86d70 100644
--- a/helm/software/components/ng_kernel/TEST
+++ b/helm/software/components/ng_kernel/TEST
@@ -38,8 +38,6 @@ Sophia-Antipolis/Buchberger: nuovo nucleo diverge
 Sophia-Antipolis/huffmann: Unknown constant
 Sophia-Antipolis/MATH/GROUPS: Unknown constant
 
-lyon: Appl con meno di due argomenti, cic:/Lyon/COINDUCTIVES/STREAMS/Alter/eqalters_III.con
-
 Rocq/ALGEBRA/CATEGORY_THEORY: vecchio nucleo
 Sophia-Antipolis/Algebra: vecchio nucleo variabili
 lyon.ok: vecchio nucleo, variabili
diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index c1b450e61..0aafc58c7 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -144,7 +144,10 @@ let splat_args ctx t n_fix rels =
         ) 
      | _,_ -> 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)
 ;;
 
 exception Nothing_to_do;;