fun _ -> ()
;;
-let lift_from k n =
+let lift_map k map =
let rec liftaux k =
let module C = Cic in
function
if m < k then
C.Rel m
else
- C.Rel (m + n)
+ C.Rel (map k m)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst
in
liftaux k
+let lift_from k n =
+ lift_map k (fun _ m -> m + n)
+
let lift n t =
if n = 0 then
t