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