+type proof_handler =
+ { get_proof: unit -> proof; (* return current proof or fail *)
+ set_proof: proof option -> unit; (* set a proof option as current proof *)
+ has_proof: unit -> bool; (* check if a current proof is available or not *)
+ new_proof: proof -> unit; (* as a set_proof but takes care also to register
+ observers *)
+ quit: unit -> unit
+ }
+