]> matita.cs.unibo.it Git - helm.git/commitdiff
Fix name capture in cofix.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 8 Apr 2008 17:51:10 +0000 (17:51 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 8 Apr 2008 17:51:10 +0000 (17:51 +0000)
helm/software/components/ng_kernel/oCic2NCic.ml

index b1b08ee3c7821db86fd7186e588c04467f7cf62f..0131b43119a31b5ad37553a4c4fe40a32d5255d6 100644 (file)
@@ -215,10 +215,10 @@ let convert_term uri t =
         in
         let bctx, fixpoints_tys, tys, _ = 
           List.fold_right 
-            (fun (name,ty,_) (ctx, fixpoints, tys, idx) -> 
+            (fun (name,ty,_) (bctx, fixpoints, tys, idx) -> 
               let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
               let r = Ref.reference_of_ouri buri(Ref.CoFix idx) 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