- | 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)) ->
+ | 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 (i,(m,(C.Irl l as irl))) as t when k > l + m ->
+ if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else t
+ | C.Meta (i,(m,l)) ->