From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 24 Jul 2009 21:23:19 +0000 (+0000)
Subject: Bug (found during code review) fixed (but not tested and bug never re-produced):
X-Git-Tag: make_still_working~3625
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc7d32fd5c34cc2ac0edff13292662585e6ffa51;p=helm.git

Bug (found during code review) fixed (but not tested and bug never re-produced):
wrong context passed around.
---

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