sig
  exception Parse_error of string
  exception Arg_expected of string * string
  exception Arg_theory_not_found of string
  exception Arg_expected_none of string
  exception Arg_pr_not_found of Decl.prsymbol
  exception Arg_qid_not_found of Ptree.qualid
  exception Arg_error of string
  exception Arg_parse_type_error of Loc.position * string * exn
  val build_naming_tables : Task.task -> Trans.naming_table
  type symbol =
      Tstysymbol of Ty.tysymbol
    | Tsprsymbol of Decl.prsymbol
    | Tslsymbol of Term.lsymbol
  val find_symbol : string -> Trans.naming_table -> Args_wrapper.symbol
  type (_, _) trans_typ =
      Ttrans : (Task.task Trans.trans, Task.task) Args_wrapper.trans_typ
    | Ttrans_l :
        (Task.task Trans.tlist, Task.task list) Args_wrapper.trans_typ
    | Tenvtrans :
        (Env.env -> Task.task Trans.trans, Task.task) Args_wrapper.trans_typ
    | Tenvtrans_l :
        (Env.env -> Task.task Trans.tlist, Task.task list)
        Args_wrapper.trans_typ
    | Tstring :
        ('a, 'b) Args_wrapper.trans_typ -> (string -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tint :
        ('a, 'b) Args_wrapper.trans_typ -> (int -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tty :
        ('a, 'b) Args_wrapper.trans_typ -> (Ty.ty -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttysymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Ty.tysymbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tprsymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Decl.prsymbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tprlist :
        ('a, 'b) Args_wrapper.trans_typ -> (Decl.prsymbol list -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tlsymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Term.lsymbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tsymbol :
        ('a, 'b) Args_wrapper.trans_typ -> (Args_wrapper.symbol -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tlist :
        ('a, 'b) Args_wrapper.trans_typ -> (Args_wrapper.symbol list -> 'a,
                                            'b)
                                           Args_wrapper.trans_typ
    | Tidentlist :
        ('a, 'b) Args_wrapper.trans_typ -> (string list -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttermlist :
        ('a, 'b) Args_wrapper.trans_typ -> (Term.term list -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttermlist_same : int *
        ('a, 'b) Args_wrapper.trans_typ -> (Term.term list -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tterm :
        ('a, 'b) Args_wrapper.trans_typ -> (Term.term -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Tformula :
        ('a, 'b) Args_wrapper.trans_typ -> (Term.term -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Ttheory :
        ('a, 'b) Args_wrapper.trans_typ -> (Theory.theory -> 'a, 'b)
                                           Args_wrapper.trans_typ
    | Topt : string *
        ('a -> 'c, 'b) Args_wrapper.trans_typ -> ('a option -> 'c, 'b)
                                                 Args_wrapper.trans_typ
    | Toptbool : string *
        ('a, 'b) Args_wrapper.trans_typ -> (bool -> 'a, 'b)
                                           Args_wrapper.trans_typ
  val wrap_l :
    ('a, Task.task list) Args_wrapper.trans_typ ->
    'a -> Trans.trans_with_args_l
  val wrap :
    ('a, Task.task) Args_wrapper.trans_typ -> 'a -> Trans.trans_with_args
  val wrap_and_register :
    desc:Pp.formatted ->
    string -> ('a, 'b) Args_wrapper.trans_typ -> 'a -> unit
  val set_argument_parsing_functions :
    Env.fformat ->
    parse_term:(Trans.naming_table -> Stdlib.Lexing.lexbuf -> Ptree.term) ->
    parse_term_list:(Trans.naming_table ->
                     Stdlib.Lexing.lexbuf -> Ptree.term list) ->
    parse_qualid:(Stdlib.Lexing.lexbuf -> Ptree.qualid) ->
    parse_list_qualid:(Stdlib.Lexing.lexbuf -> Ptree.qualid list) ->
    parse_list_ident:(Stdlib.Lexing.lexbuf -> Ptree.ident list) -> unit
end