-let r2s = function
- | 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,_) ->
- 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)
+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 string_of_implicit_annotation = function
+ | `Closed -> "▪"
+ | `Type -> ""
+ | `Hole -> "□"
+ | `Term -> "Term"
+ | `Typeof x -> "Ty("^string_of_int x^")"