module Conv: TermMono.ToFO(T1)
module Subst: Var.Subst
module P: TI.Print(T)
module U: TI.Util(T)
module Mono: TermMono.Make(T)
exception NotInFO of string
val section : Utils.Section.t
val fail_ : P.t -> string -> 'a
val failf : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
val fail_ : P.t -> string -> 'a
val conv_ty : Mono.T.t -> FO.Ty.t
val conv_var : Mono.T.t Var.t -> FO.Ty.t Var.t
val flat_arrow_ : Mono.T.t ->
Mono.T.t list * Mono.T.t
val conv_top_ty : Mono.T.t -> FO.Ty.t list * FO.Ty.t
val conv_term : sigma:U.t_ Sig.t -> Mono.T.t -> FO.T.t
val conv_form : sigma:U.t_ Sig.t -> P.t -> FO.T.t
val convert_eqns : head:TermMono.id ->
sigma:T.t Sig.t -> (T.t, T.t) Statement.equations -> FO.T.t list
val conv_attrs : Statement.decl_attr CCList.t -> FO.attr CCList.t
val convert_statement : sigma:U.t_ Sig.t ->
(P.t, U.t_) Statement.t ->
(FO.T.t, FO.Ty.t) FO.statement list
val convert_problem : (P.t, U.t_) Problem.t ->
(FO.T.t, FO.Ty.t) FO.Problem.t