(if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
| C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
let nparams =
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (_,_,nparams,_) -> nparams
| _ -> assert false in
let hes = pp ~in_type he context in
pp_exp_named_subst exp_named_subst context
| C.MutInd (uri,n,exp_named_subst) ->
(try
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
qualified_name_of_uri current_module_uri
)
| C.MutConstruct (uri,n1,n2,exp_named_subst) ->
(try
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let _,_,_,cons = get_nth dl (n1+1) in
let id,_ = get_nth cons n2 in
if patterns = [] then "assert false"
else
(let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
- (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,paramsno,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
let rc =