From e7a76b29e40fbb9dfd9c2d5a06517f6fc56f8f89 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 9 Jul 2009 07:34:37 +0000 Subject: [PATCH] Bug fixed (non-captured variable). --- helm/software/components/ng_cic_content/nTermCicContent.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 62d69f5d1..01e6fd482 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -137,8 +137,8 @@ let nast_of_cic0 eat_branch (pred n) ((name,NCic.Decl s)::ctx) t pat | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in - (Ast.Ident (name,None), Some (k ~context s)) :: cv, rhs - | _, _ -> [], k ~context pat + (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs + | _, _ -> [], k ~context:ctx pat in let j = ref 0 in let patterns = -- 2.39.2