From bc7d32fd5c34cc2ac0edff13292662585e6ffa51 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Jul 2009 21:23:19 +0000 Subject: [PATCH] Bug (found during code review) fixed (but not tested and bug never re-produced): wrong context passed around. --- helm/software/components/ng_cic_content/nTermCicContent.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 8984a4829..68733a8ef 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -153,7 +153,7 @@ let nast_of_cic0 status let rec eat_branch n ctx ty pat = match (ty, pat) with | NCic.Prod (name, s, t), _ when n > 0 -> - eat_branch (pred n) ((name,NCic.Decl s)::ctx) t pat + eat_branch (pred n) 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:ctx s)) :: cv, rhs -- 2.39.2