+let r2s pp_fix_name r =
+ try
+ match r with
+ | R.Ref (_,u,R.Ind i) ->
+ (match snd(NCicEnvironment.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
+ | _,_,_,_, 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
+ | _,_,_,_, C.Constant (_,name,_,_,_) -> name
+ | _ -> assert false)
+ | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
+ (match snd(NCicEnvironment.get_obj u) with
+ | _,_,_,_, C.Fixpoint (_,fl,_) ->
+ if pp_fix_name then
+ let _,name,_,_,_ = List.nth fl i in name
+ else
+ let name = NUri.string_of_uri u in
+ let name = Filename.basename name in
+ let name = Filename.chop_extension name in
+ name ^"("^ string_of_int i ^ ")"
+ | _ -> assert false)
+ with exn -> 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