let r2s pp_fix_name r =
try
match r with
- | R.Ref (_,u,R.Ind i) ->
- (match snd(NCicEnvironment.get_obj u) with
+ | R.Ref (_,u,R.Ind (_,i)) ->
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,name,_,_ = List.nth itl i in name
| _ -> assert false)
| R.Ref (_,u,R.Con (i,j)) ->
- (match snd(NCicEnvironment.get_obj u) with
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,_,_,cl = List.nth itl i in
let _,name,_ = List.nth cl (j-1) in name
| _ -> assert false)
| R.Ref (_,u,(R.Decl | R.Def )) ->
- (match snd(NCicEnvironment.get_obj u) with
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Constant (_,name,_,_,_) -> name
| _ -> assert false)
| R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
- (match snd(NCicEnvironment.get_obj u) with
+ (match NCicLibrary.get_obj u with
| _,_,_,_, C.Fixpoint (_,fl,_) ->
if pp_fix_name then
let _,name,_,_,_ = List.nth fl i in name