...

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index bb5862fda85f5981516944e860cd9a3db06175c3..c3dfb418c23763e8fb5d8866e7b57e837c03700f 100644 (file)
--- 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)))),
            [])