X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=01e6fd48255fc97039a06407a5d03d6088951664;hb=e7a76b29e40fbb9dfd9c2d5a06517f6fc56f8f89;hp=62d69f5d166dd979ac37bf7d99769895ef07efb0;hpb=28da21926eb9cab187ba8a64999c760083f60369;p=helm.git

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 =