UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
| C.MutInd (uri,n,exp_named_subst) ->
(try
- match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
C.InductiveDefinition (dl,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
name ^ pp_exp_named_subst exp_named_subst l
)
| C.MutConstruct (uri,n1,n2,exp_named_subst) ->
(try
- match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
C.InductiveDefinition (dl,_,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
let (id,_) = get_nth cons n2 in
)
| C.MutCase (uri,n1,ty,te,patterns) ->
let connames =
- (match fst(CicEnvironment.get_obj uri CicUniv.empty_ugraph) with
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
C.InductiveDefinition (dl,_,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
List.map (fun (id,_) -> id) cons