changed functor interface, now based on proofs instead of metasenvs (this one is...

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

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index bebea704561e44955650521708e9d2b254f34ac7..65a579b67792d608c548ae9d602d97689878e8d5 100644 (file)
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -28,16 +28,15 @@ exception Error of string
 module type Engine =
 sig
   type goal
-  type conjecture
-  type metasenv = conjecture list
+  type proof
   type tactic
 
-  val goal_of_conjecture: conjecture -> goal
-  val goal_mem: goal -> metasenv -> bool
+  val is_goal_closed: goal -> proof -> bool
+  val goals_of_proof: proof -> goal list
 
   val apply_tactic:
-    tactic -> metasenv -> goal ->
-      metasenv * goal list * goal list
+    tactic -> proof -> goal ->
+      proof * goal list * goal list (** new proof, opened goals, closed goals *)
 end
 
 module Make (E:Engine) :
@@ -45,7 +44,7 @@ sig
   type goal_switch = Open of E.goal | Closed of E.goal
   type 'a stack = 'a list
   type status =
-    E.metasenv * ((int * goal_switch) list * E.goal list * E.goal list) stack
+    E.proof * ((int * goal_switch) list * E.goal list * E.goal list) stack
 
   type tactical =
     | Tactic of E.tactic
@@ -67,6 +66,6 @@ sig
     | Qed
 
   val eval: t -> status -> status
-  val init: E.metasenv -> status
+  val init: E.proof -> status
 end