- (try lift (k-1+lift_args) (map_arg (List.nth args (n-k)))
- with Failure _ -> assert false))
- | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
- if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t
- | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m ->
- if delift && nargs <> 0 then NCic.Meta (i,(m-nargs,irl)) else t
- | NCic.Meta (i,(m,l)) ->
+ (try lift (k-1) (map_arg (List.nth args (n-k)))
+ with Failure _ | Invalid_argument _ -> assert false))
+ | C.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
+ if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
+ | C.Meta (_,(m,(C.Irl l))) as t when k > l + m -> t
+ | C.Meta (i,(m,l)) ->