exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
-let lift n =
+let lift_from k n =
let rec liftaux k =
let module C = Cic in
function
in
C.CoFix (i, liftedfl)
in
+ liftaux k
+
+let lift n t =
if n = 0 then
- (function t -> t)
+ t
else
- liftaux 1
+ lift_from 1 n t
;;
let subst arg =