sig
  val begin_module :
    ?loc:Why3.Loc.position -> ?intf:Why3.Ptree.qualid -> string -> unit
  val use : ?loc:Why3.Loc.position -> import:bool -> string list -> unit
  val add_prop :
    Why3.Decl.prop_kind ->
    ?loc:Why3.Loc.position -> string -> Why3.Ptree.term -> unit
  val add_global_var_decl : Why3.Ptree.pty -> string -> Why3.Ptree.ident
  val begin_let :
    ?ghost:bool ->
    ?diverges:bool ->
    ?ret_type:Why3.Ptree.pty -> string -> Why3.Ptree.binder list -> unit
  val add_pre : Why3.Ptree.term -> unit
  val add_writes : Why3.Ptree.term list -> unit
  val add_post : Why3.Ptree.term -> unit
  val add_body : Why3.Ptree.expr -> unit
  val end_module : unit -> unit
  val get_mlw_file : unit -> Why3.Ptree.mlw_file
end