From bb2cda4c832cf41dd6716fe59eb3161f07dfb61b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 1 May 2008 10:57:00 +0000 Subject: [PATCH] Bug fixed: application without arguments generated in case of an ens made only of variables with bodies. --- helm/software/components/ng_kernel/TEST | 2 +- helm/software/components/ng_kernel/oCic2NCic.ml | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index bae9f48d7..45867405f 100644 --- 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 6252842ff..245308d12 100644 --- 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 ;; -- 2.39.2