functor
  (C : sig
         val avoid : Typed_ast.var_avoid_f
         val env : Typed_ast.env
         val dir : string
       end) ->
  sig
    val ident_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
    val lem_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
    val hol_defs :
      Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t option
    val ocaml_defs :
      Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t option
    val isa_defs :
      Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t option
    val isa_header_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
    val coq_defs :
      Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t
    val tex_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
    val tex_inc_defs :
      Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t * Ulib.Text.t
    val html_defs : Typed_ast.def list * Ast.lex_skips -> Ulib.Text.t
    val ident_exp : Typed_ast.exp -> Ulib.Text.t
    val ident_pat : Typed_ast.pat -> Ulib.Text.t
    val ident_src_t : Types.src_t -> Ulib.Text.t
    val ident_typ : Types.t -> Ulib.Text.t
    val ident_def : Typed_ast.def -> Ulib.Text.t
  end