reference type made private, added mk_constructor to be used

[helm.git] / helm / software / components / ng_kernel / oCic2NCic.ml

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 2b59549d6178a36063c7feaebdea4275a08c5150..2244c12f826d84129facf7bc2a49fe5e493a442b 100644 (file)
--- 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