let r2s pp_fix_name r =
try
match r with
- | R.Ref (_,u,R.Ind (_,i)) ->
+ | 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)) ->
+ | R.Ref (u,R.Con (i,j)) ->
(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 )) ->
+ | R.Ref (u,(R.Decl | R.Def _)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Constant (_,name,_,_,_) -> name
| _ -> assert false)
- | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
+ | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Fixpoint (_,fl,_) ->
if pp_fix_name then