- match CicEnvironment.get_obj mutind with
- C.InductiveDefinition (tl,ingredients,r) ->
- let (_,_,arity,_) = List.nth tl i in
- (arity,r)
- | _ -> raise WrongUriToInductiveDefinition
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+ match o with
+ C.InductiveDefinition (tl,ingredients,r,_) ->
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
+ | _ -> raise WrongUriToInductiveDefinition