sig
  val gen_extra_level : int Pervasives.ref
  module Make :
    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
end