From 1eb2e2dea4fdccd5378c92da179606d897cc61ce Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Mar 2008 15:59:51 +0000 Subject: [PATCH] context for fixpoint body created in the hopefully right order --- 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 2f95d663c..b900d169b 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -77,7 +77,7 @@ let convert_term uri t = (fun (name,ty,_) (ctx, fixpoints, tys, idx) -> let ty, fixpoints_ty = aux octx ctx n_fix uri ty in let r = NReference.reference_of_ouri buri(NReference.CoFix idx) in - ctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx+1) + Fix (r,name,ty) :: ctx, fixpoints_ty @ fixpoints,ty::tys,idx+1) fl ([], [], [], 0) in let bctx = bctx @ ctx in @@ -119,7 +119,7 @@ let convert_term uri t = let r = NReference.reference_of_ouri buri (NReference.Fix (idx,recno)) in - ctx @ [Fix (r,name,ty)], fixpoints_ty@fixpoints,ty::tys,idx+1) + Fix (r,name,ty) :: ctx, fixpoints_ty@fixpoints,ty::tys,idx+1) fl ([], [], [], 0) in let bctx = bctx @ ctx in -- 2.39.2