From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 19 Feb 2008 17:05:43 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~5594
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b26e58af5174439d90a5a45675530d3c1a136147;p=helm.git

...
---

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)))),
            [])