| _ -> assert false
let get_types uri =
- match CicEnvironment.get_obj uri with
- | Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
+ let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
+ | Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,_) -> l
let name_of_inductive_type uri i =
let types = get_types uri in