Bug fixed: application without arguments generated in case of an ens made only

of variables with bodies.

diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST
index bae9f48d78ae1fe6aa8f3383693001e21f0a771d..45867405f3d29c5c4349dbe8ddd1792c7bf4021b 100644 (file)
--- a/helm/software/components/ng_kernel/TEST
+++ b/helm/software/components/ng_kernel/TEST
@@ -38,7 +38,7 @@ 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_body.con
+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

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 6252842ff0a4d6f7c2d8ff9a1596f8f36e457215..245308d12235e346599b1940e9e16ed48b8aa900 100644 (file)
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -595,7 +595,9 @@ let convert_term uri t =
            | _ -> assert false
         ) params ([],[])
       in
-       NCic.Appl (he::ens),objs
+       match ens with
+          [] -> he,objs
+        | _::_ -> NCic.Appl (he::ens),objs
   in
    aux false [] [] 0 uri t
 ;;