- added stack frame tagging

[helm.git] / helm / ocaml / tactics / continuationals.mli

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 65a579b67792d608c548ae9d602d97689878e8d5..e89e2e51d17e6734d31cefe93dc9d1cf5f2a297c 100644 (file)
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -39,15 +39,16 @@ sig
       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 =
@@ -56,16 +57,27 @@ sig
 
     | 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
+