From b26e58af5174439d90a5a45675530d3c1a136147 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 Feb 2008 17:05:43 +0000 Subject: [PATCH] ... --- helm/software/components/ng_kernel/oCic2NCic.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index bb5862fda..c3dfb418c 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -102,8 +102,10 @@ let convert_term uri t = | Cic.Rel n -> (match List.nth ctx n with | Ce _ -> NCic.Rel (n-n_fix), [] - | Fix (recno, fixno) -> - splat_args ctx + | Fix (recno, fixno) -> + (* uri should be in the context, since the inner + * fix may refer to the outer one *) + splat_args ctx (* this function must lift the args wrt len(octx) *) (NCic.Const (NReference.reference_of_ouri uri (NReference.Fix (fixno,recno)))), []) -- 2.39.2