-(** {2 tactic commands builders} *)
-
-(* TODO Zack: these are just some examples, a lot of other tactics/tacticals
- * must be added here *)
-
-val intros: ?namer:MatitaTypes.namer ->
- MatitaTypes.proofStatus -> MatitaTypes.command
-
-val reflexivity: MatitaTypes.proofStatus -> MatitaTypes.command
-val symmetry: MatitaTypes.proofStatus -> MatitaTypes.command
-val transitivity: Cic.term -> MatitaTypes.proofStatus -> MatitaTypes.command
-
-val exists: MatitaTypes.proofStatus -> MatitaTypes.command
-val split: MatitaTypes.proofStatus -> MatitaTypes.command
-val left: MatitaTypes.proofStatus -> MatitaTypes.command
-val right: MatitaTypes.proofStatus -> MatitaTypes.command
-
-val assumption: MatitaTypes.proofStatus -> MatitaTypes.command
+ (** current proof handler *)
+class type 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
+
+val currentProof: unit -> currentProof
+
+ (** currentProof singleton instance *)
+val instance: unit -> currentProof