sig
  type non_ident_target =
      Target_hol
    | Target_ocaml
    | Target_isa
    | Target_coq
    | Target_tex
    | Target_html
    | Target_lem
  type target = Target_no_ident of Target.non_ident_target | Target_ident
  val ast_target_to_target : Ast.target -> Target.non_ident_target
  val target_to_ast_target : Target.non_ident_target -> Ast.target
  val ast_target_compare : Ast.target -> Ast.target -> int
  val target_compare :
    Target.non_ident_target -> Target.non_ident_target -> int
  module Targetmap :
    sig
      type k = non_ident_target
      module S :
        sig
          type elt = k
          type t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
          val split : elt -> t -> t * bool * t
        end
      type 'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val from_list : (k * 'a) list -> 'a t
      val from_list2 : k list -> 'a list -> 'a t
      val insert : 'a t -> k * 'a -> 'a t
      val union : 'a t -> 'a t -> 'a t
      val big_union : 'a t list -> 'a t
      val merge :
        (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val apply : 'a t -> k -> 'a option
      val in_dom : k -> 'a t -> bool
      val map : (k -> 'a -> 'b) -> 'a t -> 'b t
      val domains_overlap : 'a t -> 'b t -> k option
      val domains_disjoint : 'a t list -> bool
      val iter : (k -> 'a -> unit) -> 'a t -> unit
      val fold : ('a -> k -> 'b -> 'a) -> 'a -> 'b t -> 'a
      val filter : (k -> 'a -> bool) -> 'a t -> 'a t
      val remove : 'a t -> k -> 'a t
      val pp_map :
        (Format.formatter -> k -> unit) ->
        (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
      val domain : 'a t -> S.t
      val apply_target : 'a t -> Target.target -> 'a option
      val insert_target : 'a t -> Target.target * 'a -> 'a t
    end
  module Targetset :
    sig
      type elt = non_ident_target
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
    end
  val all_targets_list : Target.non_ident_target list
  val all_targets : Target.Targetset.t
  val all_targets_non_explicit : Target.Targetset.t
  val non_ident_target_to_string : Target.non_ident_target -> string
  val target_to_string : Target.target -> string
  val non_ident_target_to_mname : Target.non_ident_target -> Name.t
  val target_to_output : Ast.target -> Output.t
  val is_human_target : Target.target -> bool
  val dest_human_target : Target.target -> Target.non_ident_target option
end