- better naming

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

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 4b2632e56c232d77aa6126e1adfee6c789ef5084..bebea704561e44955650521708e9d2b254f34ac7 100644 (file)
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -33,7 +33,7 @@ sig
   type tactic
 
   val goal_of_conjecture: conjecture -> goal
-  val is_goal_in_metasenv: metasenv -> goal -> bool
+  val goal_mem: goal -> metasenv -> bool
 
   val apply_tactic:
     tactic -> metasenv -> goal ->
@@ -54,13 +54,19 @@ sig
   type t =
     | Dot
     | Semicolon
+
     | Branch
     | Shift of int option
     | Merge
+
     | Select of E.goal list
     | End_select
+
     | Tactical of tactical
 
+    | Qed
+
   val eval: t -> status -> status
+  val init: E.metasenv -> status
 end