sig type pred type decl val export_section : Format.formatter -> string -> unit val export_goal : Format.formatter -> string -> Wp.Mcfg.Export.pred -> unit val export_decl : Format.formatter -> Wp.Mcfg.Export.decl -> unit end