-(* CODICE c&p da NCicPp *)
-let r2s pp_fix_name r =
- try
- match r with
- | NReference.Ref (u,NReference.Ind (_,i,_)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
- let _,name,_,_ = List.nth itl i in name
- | _ -> assert false)
- | NReference.Ref (u,NReference.Con (i,j,_)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Inductive (_,_,itl,_) ->
- let _,_,_,cl = List.nth itl i in
- let _,name,_ = List.nth cl (j-1) in name
- | _ -> assert false)
- | NReference.Ref (u,(NReference.Decl | NReference.Def _)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Constant (_,name,_,_,_) -> name
- | _ -> assert false)
- | NReference.Ref (u,(NReference.Fix (i,_,_)|NReference.CoFix i)) ->
- (match NCicLibrary.get_obj u with
- | _,_,_,_, NCic.Fixpoint (_,fl,_) ->
- if pp_fix_name then
- let _,name,_,_,_ = List.nth fl i in name
- else
- NUri.name_of_uri u ^"("^ string_of_int i ^ ")"
- | _ -> assert false)
- with NCicLibrary.ObjectNotFound _ -> NReference.string_of_reference r