X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=2244c12f826d84129facf7bc2a49fe5e493a442b;hb=3c8abd24ff28dfd95f1428dae80c5807a328e9ae;hp=2b59549d6178a36063c7feaebdea4275a08c5150;hpb=79501fecaa51e1afff2ac940706b4490b368dc27;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 2b59549d6..2244c12f8 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -113,13 +113,13 @@ let convert_term uri t =
         let rno = ref 0 in
         let bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
-            (fun (name,recno,ty,_) (ctx, fixpoints, tys, idx) -> 
+            (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) -> 
               let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
               if idx = k then rno := recno;
               let r = 
                 NReference.reference_of_ouri buri (NReference.Fix (idx,recno)) 
               in
-              Fix (r,name,ty) :: ctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
+              Fix (r,name,ty) :: bctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
             fl ([], [], [], 0)
         in
         let bctx = bctx @ ctx in