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 =