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 45867405f3d29c5c4349dbe8ddd1792c7bf4021b..7abd86d703cf32d27ead2354d2c610904122b482 100644 (file)
--- 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 c1b450e612d627135a6f982dbbb2088d8c12b1cb..0aafc58c7a752f35a0b65175d10a9cba4e466cc2 100644 (file)
--- 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;;