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 (i,(m,(C.Irl l as irl))) as t when k > l + m -> t
+ | C.Meta (_,(m,(C.Irl l))) as t when k > l + m -> t
| C.Meta (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
C.Meta (i,(0,