From 7bb53e63c15cf501c98881839a2fdc19a6c88028 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 1 May 2008 14:11:07 +0000 Subject: [PATCH] Last (???) bug about variables with bodies fixed: we do no longer create applications with less than 2 args. --- helm/software/components/ng_kernel/TEST | 2 -- helm/software/components/ng_kernel/oCic2NCic.ml | 5 ++++- 2 files changed, 4 insertions(+), 3 deletions(-) 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;; -- 2.39.2