exception Arg_trans_decl of string * Theory.tdecl listexception Arg_trans_term of string * Term.termexception Arg_trans_pattern of string * Term.pattern * Term.patternexception Arg_bad_hypothesis of string * Term.termexception Unnecessary_terms of Term.term listval gen_ident :
?attrs:Ident.Sattr.t ->
?loc:Loc.position ->
string ->
Ident.preidval subst_quant : Term.quant -> Term.term_quant -> Term.term -> Term.termval get_local : Decl.decl list Trans.transval sort : Task.task Trans.transval add_goal_attr_trans : Ident.attribute -> Task.task Trans.transtype term_subst = Term.term Term.Mterm.tval replace_subst : term_subst -> Term.term -> Term.termval replace_decl : term_subst -> Decl.decl -> Decl.declval replace_tdecl : term_subst -> Theory.tdecl -> Theory.tdecl