unit ->
MatitaTypes.proof
+ (** current proof handler *)
+class currentProof:
+ object
+ inherit MatitaTypes.currentProof
+
+ (** add an observer to the current observer list. All observers will be
+ * attached to each new proof (method "start") created by this object
+ *)
+ method addObserver: unit StatefulProofEngine.observer -> unit
+
+ (** connect as the first event handler for a given event (abort or quit).
+ * If the event handler returns true, handler processing stops, otherwise
+ * continue with the next handler
+ *)
+ method connect: [`Abort|`Quit] -> (unit -> bool) -> unit
+ end
+