let lift_from status ?(no_implicit=true) k n =
let rec liftaux k = function
| C.Rel m as t -> if m < k then t else C.Rel (m + n)
let lift_from status ?(no_implicit=true) k n =
let rec liftaux k = function
| C.Rel m as t -> if m < k then t else C.Rel (m + n)