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 =
with
Not_found ->
let params =
- let obj = CicEnvironment.get_obj uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable (_,_,_,params) -> params
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst') ->
let params =
- let obj = CicEnvironment.get_obj uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
C.Constant (_,_,_,params) -> params
| C.Variable _ -> raise ReferenceToVariable
C.Const (uri,exp_named_subst'')
| C.MutInd (uri,typeno,exp_named_subst') ->
let params =
- let obj = CicEnvironment.get_obj uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
C.MutInd (uri,typeno,exp_named_subst'')
| C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
let params =
- let obj = CicEnvironment.get_obj uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable