sig
  val reset : unit -> unit
  val set : string -> unit
  val is_set : unit -> bool
  val iter :
    (qed:Wp.Lang.F.term -> raw:Wp.Lang.F.term -> goal:Wp.Lang.F.pred -> unit) ->
    unit
end