k ~context:((n,NCic.Decl s)::context) t))
| NCic.LetIn (n,s,ty,NCic.Rel 1) ->
idref (Ast.Cast (k ~context ty, k ~context s))
| NCic.LetIn (n,s,ty,t) ->
k ~context:((n,NCic.Decl s)::context) t))
| NCic.LetIn (n,s,ty,NCic.Rel 1) ->
idref (Ast.Cast (k ~context ty, k ~context s))
| NCic.LetIn (n,s,ty,t) ->