proof * goal list * goal list (** new proof, opened goals, closed goals *)
end
-module Make (E:Engine) :
+module type C =
sig
- type goal_switch = Open of E.goal | Closed of E.goal
- type 'a stack = 'a list
- type status =
- E.proof * ((int * goal_switch) list * E.goal list * E.goal list) stack
+ type goal
+ type proof
+ type tactic
+
+ type status
type tactical =
- | Tactic of E.tactic
+ | Tactic of tactic
| Skip
type t =
| Branch
| Shift of int option
- | Merge
-
- | Select of E.goal list
- | End_select
+ | Select of goal list
+ | End
| Tactical of tactical
- | Qed
-
val eval: t -> status -> status
- val init: E.proof -> status
+ val init: proof -> status
+
+ (** {2 Status accessors} *)
+
+ val get_proof: status -> proof
+ val set_proof: proof -> status -> status
+
+ type goal_switch = Open of goal | Closed of goal
+ val get_goals: status -> goal_switch list
+
+ val is_completed: status -> bool
end
+module Make (E:Engine) : C
+ with type goal = E.goal
+ and type proof = E.proof
+ and type tactic = E.tactic
+