let lift_from k n =
let rec liftaux k = function
| C.Rel m as t -> if m < k then t else C.Rel (m + n)
+ | C.Meta (i,(m,(C.Irl 0 as l))) when k <= m+1 -> C.Meta (i,(m,l))
| C.Meta (i,(m,l)) when k <= m+1 -> C.Meta (i,(m+n,l))
| C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
| C.Meta (i,(m,l)) ->
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 ->
- if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else 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,