+val all_events: event list
+
+ (** from our point of view a status is the status of an incomplete proof, thus
+ * we have an optional goal which is None if the proof is not yet completed
+ * (i.e. some goal is still open) *)
+type proof_status = ProofEngineTypes.proof * ProofEngineTypes.goal option
+