match !current_proof with
| Some proof -> proof
| None -> failwith "No current proof"),
- (fun proof -> current_proof := proof),
+ (fun proof -> (* TODO Zack: this function should probably be smarter taking
+ care also of unregistering notifications subscriber and so on *)
+ current_proof := proof),
(fun () -> !current_proof <> None))
(** {2 Settings} *)