let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
C.Constant _ -> raise ReferenceToConstant
- | C.Variable (_,_,_,params) -> params
+ | C.Variable (_,_,_,params,_) -> params
| C.CurrentProof _ -> raise ReferenceToCurrentProof
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
let params =
let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(match obj with
- C.Constant (_,_,_,params) -> params
+ C.Constant (_,_,_,params,_) -> params
| C.Variable _ -> raise ReferenceToVariable
- | C.CurrentProof (_,_,_,_,params) -> params
+ | C.CurrentProof (_,_,_,_,params,_) -> params
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
in
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_) -> params
+ | C.InductiveDefinition (_,params,_,_) -> params
)
in
let exp_named_subst'' =
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof _ -> raise ReferenceToCurrentProof
- | C.InductiveDefinition (_,params,_) -> params
+ | C.InductiveDefinition (_,params,_,_) -> params
)
in
let exp_named_subst'' =