sig
  val dexpr :
    Why3.Pmodule.pmodule_uc ->
    Why3.Dexpr.denv -> Why3.Ptree.expr -> Why3.Dexpr.dexpr
  val drec_defn :
    Why3.Pmodule.pmodule_uc ->
    Why3.Dexpr.denv ->
    Why3.Ptree.fundef list -> Why3.Dexpr.denv * Why3.Dexpr.drec_defn
  val add_decl :
    Why3.Pmodule.pmodule_uc ->
    Why3.Env.env ->
    Why3.Pmodule.mlw_file -> Why3.Ptree.decl -> Why3.Pmodule.pmodule_uc
  val create_user_id : Why3.Ptree.ident -> Why3.Ident.preid
  val create_user_prog_id : Why3.Ptree.ident -> Why3.Ident.preid
end