if sort = `Prop then
let inductive_types =
(let o,_ =
- CicEnvironment.get_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
in
match o with
| Cic.InductiveDefinition (l,_,_,_) -> l
else raise Not_a_proof
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
let inductive_types,noparams =
- (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
let ind_str = (prefix ^ ".ind") in
let ind_uri = UriManager.uri_of_string ind_str in
let inductive_types,noparams =
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
match o with
| Cic.InductiveDefinition (l,_,n,_) -> (l,n)
| _ -> assert false