From 69f947f6256eaf028c673c6a2327a935c4b3465a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 17:51:10 +0000 Subject: [PATCH] Fix name capture in cofix. --- helm/software/components/ng_kernel/oCic2NCic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index b1b08ee3c..0131b4311 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -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 -- 2.39.2