+let r2s pp_fix_name r =
+ try
+ match r 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 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 NCicLibrary.get_obj u with
+ | _,_,_,_, C.Constant (_,name,_,_,_) -> name
+ | _ -> assert false)
+ | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) ->
+ (match NCicLibrary.get_obj u with
+ | _,_,_,_, C.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 _ -> R.string_of_reference r
+;;
+
+let trivial_pp_term ~context ~subst:_ ~metasenv:_ ?(inside_fix=false) t =
+ let buff = Buffer.create 100 in
+ let f = Format.formatter_of_buffer buff in
+ let module F = Format in
+ let rec aux ?(toplevel=false) ctx = function