From 46219a352fd586e1f89237effdcb037a6e371969 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 1 May 2008 13:59:06 +0000 Subject: [PATCH] Another case where the presence of variables with bodies resulted in the creation of an application without arguments. --- helm/software/components/ng_kernel/oCic2NCic.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 245308d12..c1b450e61 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -121,7 +121,10 @@ let splat_args_for_rel ctx t ?rels n_fix = | `Ce ((_, NCic.Def _),_) -> aux (n-1,tl)) | _,_ -> 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) ;; let splat_args ctx t n_fix rels = -- 2.39.2